Verification of a Turntable System

Organisation:	Université catholique de Louvain (BELGIUM)
Method:	LOTOS NuSMV language
Tools used:	CADP (Construction and Analysis of Distributed Processes) NuSMV FwdUntilPOR model checker
Domain:	Industrial Manufacturing Systems.
Period:	2009
Size:	n/a
Description:	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.
Conclusions:	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.
Publications:	[Meulen-Pecheur-09] 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 the CADP Web site in PDF or PostScript
Contact:	Prof. Charles Pecheur Dept. INGI Université catholique de Louvain Place Sainte-Barbe 2 1348 Louvain-la-Neuve BELGIUM Tel: +32 10 47 87 79 Fax: +32 10 45 03 45 Email: [email protected]
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page