Université catholique de Louvain (BELGIUM)
CADP (Construction and Analysis of Distributed Processes)
FwdUntilPOR model checker
Industrial Manufacturing Systems.
Model checking is a technique used to verify concurrent systems, such
as sequential circuit designs and communication protocols, by
exhaustively exploring the state space of a finite-state description
of the processes involved. Unfortunately, the size of the state space
to be explored is frequently prohibitive due to, among other causes,
the modeling of concurrency by interleaving. Several techniques
have been proposed to combat state explosion, amongst which the use of
ordered Binary Decision Diagrams (BDDs) to represent symbolically sets
of states, and of partial order reductions (POR) to reduce the number
of interleaving sequences that must be considered.
This work proposes a new algorithm, named FwdUntilPOR, that combines BDD-based model checking with partial order reduction (POR) to allow the verification of models featuring asynchronous processes, with significant performance improvements over currently available tools. The algorithm has been implemented in a prototype model checker that is applicable to action-based models and logics such as LOTOS and ACTL.
This new model checker has been applied to the analysis of a turntable system, which consists of a round turntable, n drills and a testing device. The turntable transports products between the drills, the testing device and input and output positions. The drills bore holes in the products. After being drilled, the products are delivered to the tester, where the depth of the holes is measured, since it is possible that drilling went wrong. The turntable has n+3 slots that each can hold a single product. Starting from an original model in LOTOS, a NuSMV model was derived, and subsequently converted into the input language of the model checker. Three verification methods were used: classical backward, FwdUntil and FwdUntil with POR, as well as with the NuSMV tool and with the explicit-state model checker EVALUATOR of CADP. A number of 13 correctness properties were verified, on turntable configurations containing up to 40 drills. The new algorithm FwdUntilPOR exhibits strong improvements in comparison to the classical algorithms, in a majority of cases.
Although it is usually considered that symbolic model checking is
inadequate for loosely-synchronized models, the results obtained show
that with appropriate optimization this approach might in fact be quite
effective to tackle the state space explosion problem.
Jose Vander Meulen and Charles Pecheur.
"Efficient Symbolic Model Checking for Process Algebras".
Proceedings of the 13th International Workshop on Formal Methods
for Industrial Critical Systems FMICS'2008, Lecture Notes in Computer
Science vol. 5596, pages 69-84. Springer Verlag, September 2009.
Available on-line at: http://www.info.ucl.ac.be/~pecheur/publi/FWD_ImProviso.pdf
or from our FTP site in PDF or PostScript
Prof. Charles Pecheur
Université catholique de Louvain
Place Sainte-Barbe 2
Tel: +32 10 47 87 79
Fax: +32 10 45 03 45
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|