×

zbMATH — the first resource for mathematics

Bounded model checking of traffic light control system. (English) Zbl 1351.68169
Xue, Jinyun (ed.) et al., Proceedings of the 6th international workshop on harnessing theories for tool support in software (TTSS 2013), Nanchang, China, October 27, 2013. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 309, 63-74, electronic only (2014).
Summary: Traffic Light Control System (TLCS) is widely used in our daily life. It is of great importance to ensure the correctness of TLCS. In this paper, bounded model checking (BMC) is chosen to verify a simple but practical TLCS. To this end, Propositional Projection Temporal Logic (PPTL) used as the property specification language and the process of BMC for PPTL are briefly introduced. Then, a TLCS is described and its corresponding Kripke structure is given. Finally, two related properties specified by PPTL formulas are verified for the system using the BMC approach. The verification result using our bounded model checker, BMC4PPTL, shows that the behavior of TLCS is consistent with the specification.
For the entire collection see [Zbl 1310.68021].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
90B20 Traffic problems in operations research
Software:
NuSMV; SPIN
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Biere, A.; Cimatti, A.; Clarke, E. M.; Strichman, O.; Zhu, Y., Bounded model checking, Advances in computers, 58, 117-148, (2003)
[2] Burch, J. R.; Clarke, E. M.; McMillan, K. L.; Dill, D. L.; Hwang, L.-J., Symbolic model checking: 1020 states and beyond, Information and computation, 98, 142-170, (1992) · Zbl 0753.68066
[3] R. Cavda, A. Cimatti, C.A. Jochim, G. Keighren, E. Olivetti, M. Pistore, M. Roveri, A. Tchaltsev, Nusmv 2.5 user manual, 2010.
[4] Clarke, E. M.; Emerson, E., Design and synthesis of synchronization skeletons using branching time temporal logic, Logics of Programs, 52-71, (1982) · Zbl 0546.68014
[5] Clarke, E. M.; Grumberg, O.; Long, D. E., Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), 16, 1512-1542, (1994)
[6] Clarke, E. M.; Grumberg, O.; Peled, D. A., Model checking, (1999), MIT press
[7] Clarke, E. M.; Long, D. E.; McMillan, K. L., Compositional model checking, (Proceedings of the 4th Annual Symposium on Logic in Computer Science, (1989), IEEE), 353-362 · Zbl 0716.68035
[8] Coudert, O.; Madre, J. C., A unified framework for the formal verification of sequential circuits, (Proceedings of the 1990 International Conference on Computer-Aided Design, (1990), IEEE), 126-129
[9] Duan, Z., An extended interval temporal logic and a framing technique for temporal logic programming, (1996), University of Newcastle upon Tyne, Ph.D. thesis
[10] Duan, Z., Temporal logic and temporal logic programming, (2005), Science Press
[11] Duan, Z.; Koutny, M.; Holt, C., Projection in temporal logic programming, (Logic Programming and Automated Reasoning, Upon Type, vol. 10, (1994), Springer), 333-344, (A technical report No. 452, University of Newcastle Upon Type, 10, 1993, is available)
[12] Duan, Z.; Tian, C.; Yang, M.; He, J., Bounded model checking for propositional projection temporal logic, (Computing and Combinatorics, (2013), Springer), 591-602 · Zbl 1382.68141
[13] Duan, Z.; Tian, C.; Zhang, L., A decision procedure for propositional projection temporal logic with infinite models, Acta Informatica, 45, 43-78, (2008) · Zbl 1141.68039
[14] G. Holtzman, The spin model checker, primer and reference manual, 2003.
[15] McMillan, K. L., Symbolic model checking, (1993), Springer · Zbl 0784.68004
[16] Pnueli, A., The temporal logic of programs, (Proceedings of the 18th Annual Sympostum on the Foundations of Computer Science, (1977), IEEE), 46-57
[17] Tian, C.; Duan, Z., Propositional projection temporal logic, Büchi automata and ω-regular expressions, (Theory and Applications of Models of Computation, (2008), Springer), 47-58 · Zbl 1140.03305
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.