Abstract
Modern reactive control system are typically very complex entities, and their design poses substantial challenges. In addition to ensuring functional correctness, other steps may be required: with safety analysis, the behavior is analyzed, and proved compliant to some requirements considering possible faulty behaviors; diagnosis and diagnosability are forms of reasoning on the run-time explanation of faulty behaviors; planning and synthesis allow the automated construction of controllers that implement desired behaviors. Symbolic Model Checking (SMC) is a formal technique for ensuring functional correctness that has achieved a substantial industrial penetration in the last decade. In this paper, we show how SMC can be used as a convenient framework to express safety analysis, diagnosis and diagnosability, and synthesis. We also discuss how model checking tools can be used and extended to solve the resulting computational challenges.
This work has been partly supported by the E.U.-sponsored project ISAAC, contract no. AST3-CT-2003-501848.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Åkerlund, O., Bieber, P., Böede, E., Bozzano, M., Bretschneider, M., Castel, C., Cavallo, A., Cifaldi, M., Gauthier, J., Griffault, A., Lisagor, O., Lüdtke, A., Metge, S., Papadopoulos, C., Peikenkamp, T., Sagaspe, L., Seguin, C., Trivedi, H., Valacca, L.: ISAAC, a framework for integrated safety analysis of functional, geometrical and human aspects. In: Proc. European Congress on Embedded Real Time Software (ERTS 2006) (2006)
Banach, R., Bozzano, M.: Retrenchment, and the Generation of Fault Trees for Static, Dynamic and Cyclic Systems. In: Gorski, J. (ed.) SAFECOMP 2006. LNCS, vol. 4166, pp. 127–141. Springer, Heidelberg (2006)
Bertoli, P., Cimatti, A., Pistore, M.: Strong Cyclic Planning under Partial Observability. In: Proc. of 17th European Conference on Artificial Intelligence (ECAI 2006) (2006)
Bertoli, P., Cimatti, A., Pistore, M., Traverso, P.: A Framework for Planning with Extended Goals under Partial Observability. In: Proc. International Conference on Automated Planning and Scheduling (ICAPS 2003) (2003)
Bertoli, P., Cimatti, A., Roveri, M., Traverso, P.: Strong Planning under Partial Observability. Artificial Intelligence 170, 337–384 (2006)
Biere, A., Cimatti, A., Clarke, E., Fujita, M., Zhu, Y.: Symbolic Model Checking Using SAT Procedures instead of BDDs. In: Proceedings of the 36th Design Automation Conference (DAC 1999), New Orleans, LA, USA, pp. 317–320. ACM Press, New York (1999)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Bonet, B., Geffner, H.: Planning with Incomplete Information as Heuristic Search in Belief Space. In: Proc. 5th International Conference on Artificial Intelligence Planning and Scheduling (AIPS 2000), pp. 52–61 (2000)
Bozzano, M., Cavallo, A., Cifaldi, M., Valacca, L., Villafiorita, A.: Improving Safety Assessment of Complex Systems: An industrial case study. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 208–222. Springer, Heidelberg (2003)
Bozzano, M., Villafiorita, A.: The FSAP/NuSMV-SA Safety Analysis Platform. International Journal on Software Tools for Technology Transfer, 2006. DOI 10.1007/s10009-006-0001-2 (to appear)
Bozzano, M., Villafiorita, A., Åkerlund, O., Bieber, P., Bougnol, C., Böde, E., Bretschneider, M., Cavallo, A., Castel, C., Cifaldi, M., Cimatti, A., Griffault, A., Kehren, C., Lawrence, B., Lüdtke, A., Metge, S., Papadopoulos, C., Passarello, R., Peikenkamp, T., Persson, P., Seguin, C., Trotta, L., Valacca, L., Zacco, G.: ESACS: An Integrated Methodology for Design and Safety Analysis of Complex Systems. In: Proc. European Safety and Reliability Conference (ESREL 2003), pp. 237–245. Balkema Publisher, 2003
Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)
Bryant, R.E.: Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys 24(3), 293–318 (1992)
Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.L.: Symbolic Model Checking for Sequential Circuit Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 13(4), 401–424 (1994)
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(2), 142–170 (1992)
Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Cimatti, A., Pecheur, C., Cavada, R.: Formal Verification of Diagnosability via Symbolic Model Checking. In: Gottlob, G., Walsh, T. (eds.) Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI 2003), Acapulco, Mexico, pp. 363–369. Morgan Kaufmann, San Francisco (2003)
Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Weak, Strong, and Strong Cyclic Planning via Symbolic Model Checking. Artificial Intelligence 147(1-2), 35–84 (2003)
Cimatti, A., Roveri, M., Bertoli, P.: Conformant Planning via Symbolic Model Checking and Heuristic Search. Artificial Intelligence 159, 127–206 (2004)
Cimatti, A., Roveri, M., Traverso, P.: Strong Planning in Non-Deterministic Domains via Model Checking. In: Proc. 4th International Conference on Artificial Intelligence Planning Systems (AIPS- 1998), Carnegie Mellon University, Pittsburgh, USA, AAAI-Press, Stanford, California, USA (1998)
Clarke, E.M., Emerson, E.A.: Synthesis of Synchronization Skeletons for Branching Time Temporal Logic. In: Kozen, D. (ed.) Logics of Programs. LNCS, vol. 131, Springer, Heidelberg (1982)
Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)
Clarke, E.M., Grumberg, O., Hiraishi, H., Jha, S., Long, D., McMillan, K.L., Ness, L.: Verification of the FUTUREBUS+ Cache Coherence Protocol. In: Proc. of 11th International Symposium on Computer Hardware Description Languages and their Applications (CHDL-1993) (1993)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge, MA (1999)
Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 436–453. Springer, Heidelberg (2001)
Coudert, O., Berthet, C., Madre, J.C.: Verification of Synchronous Sequential Machines Using Symbolic Execution. In: Proc. of International Workshop on Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, Springer, Heidelberg (1989)
Coudert, O., Madre, J.C.: Fault Tree Analysis: 1020 Prime Implicants and Beyond. In: Proc. Annual Reliability and Maintainability Symposium (RAMS 1993) (1993)
Dal Lago, U., Pistore, M., Traverso, P.: Planning with a Language for Extended Goals. In: Proc. 18th National Conference on Artificial Intelligence (AAAI 2002) (2002)
Dill, D.L., Drexler, A J., Hu, A.J., Yang, C.H.: Protocol Verification as a Hardware Design Aid. In: International Conference on Computer Design, VLSI in Computers and Processors, pp. 522–525. IEEE Computer Society Press, Los Alamitos, Ca., USA (October 1992)
Eèn, N., Sörensson, N.: An extensible sat solver. In: Proc. of the 6th International Conference on Theory and Applications of Satisfiability Testing, pp. 502–518 (2003)
Emerson, E.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, vol. B, Formal Models and Semantics, Elsevier, Amsterdam (1990)
Fikes, R.E., Nilsson, N.J.: STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving. Artificial Intelligence 2, 187–208 (1971)
The FSAP platform. http://sra.itc.it/tools/FSAP
Ghallab, M., Nau, D., Traverso, P.: Automated Planning: Theory and Practice. 1, pp. 17–110. Morgan Kaufmann, Washington (2004)
Gupta, A., Clarke, E., Strichman, O.: Sat based counterexample-guided abstraction-refinement. IEEE Transactions on Computer Aided Design 23, 1113–1123 (2004)
Heljanko, K., Junttila, T.A., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 98–111. Springer, Heidelberg (2005)
Hoffmann, J., Brafman, R.: Contingent Planning via Heuristic Forward Search with Implicit Belief States. In (ICAPS-2005). Proc. of 15th International Conference on Automated Planning and Scheduling, Monterey, CA, USA, pp. 71–80. Kaufmann, San Francisco (2005)
Holzmann, G.J.: The model checker Spin. IEEE Trans. on Software Engineering, Special issue on Formal Methods in Software Practice. 23(5), 279–295 (1997)
Jiang, S., Huang, Z., Chandra, V., Kumar, R.: A polynomial algorithm for testing diagnosability of discrete event systems. IEEE Transactions on Automatic Control 46(8), 1318–1321 (2001)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
The NuSMV model checker, http://nusmv.itc.it
Pistore, M., Traverso, P.: Planning as Model Checking for Extended Goals in Non-deterministic Domains. In: Proc. of 17th International Joint Conference on Artificial Intelligence (IJCAI-2001) (2001)
Pixley, C.: A Computational Theory and Implementation of Sequential Hardware Equivalence. In: DIMACS Workshop on Computer Aided Verification ’90, Providence, RI pp. 293–320 (1990)
Prasad, M., Biere, A., Gupta, A.: A survey of recent advances in sat-based formal verification. STTT (7), 156–173 (2005)
Queille, J.P., Sifakis, J.: Specification and Verification of Concurrent Systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol. 137, pp. 337–371. Springer, Heidelberg (1982)
Rauzy, A.: New Algorithms for Fault Trees Analysis. Reliability Engineering and System Safety 40(3), 203–211 (1993)
Rintanen, J.: Backward Plan Construction for Planning as Search in Belief Space. In: Proc. of 6th International Conference on Artificial Intelligence Planning and Scheduling (AIPS 2002), pp. 93–102 (2002)
Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of discrete-event systems. IEEE Transactions on Automatic Control 40(9), 1555–1575 (1995)
Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Failure diagnosis using discrete event models. IEEE Transactions on Control Systems 4(2), 105–124 (1996)
Sheeran, M., Singh, S., Stalmarck, G.: Checking safety properties using induction and a sat-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, Springer, Heidelberg (2000)
Siu, N.O.: Risk Assessment for Dynamic Systems: An Overview. Reliability Engineering and System Safety 43, 43–74 (1994)
Touati, H.J., Savoj, H., Lin, B., Brayton, R.K., Sangiovanni-Vincentelli, A.: Implicit State Enumeration of Finite State Machines Using BDDs. In: Proc. of the IEEE International Conference on Computer-Aided Design, pp. 130–133, Santa Clara, CA , IEEE Computer Society Press, Los Alamitos (November 1990)
Vesely, W.E., Goldberg, F.F., Roberts, N.H., Haasl, D.F.: Fault Tree Handbook. Technical Report NUREG-0492, Systems and Reliability Research Office of Nuclear Regulatory Research U.S. Nuclear Regulatory Commission (1981)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bertoli, P., Bozzano, M., Cimatti, A. (2007). A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis. In: Edelkamp, S., Lomuscio, A. (eds) Model Checking and Artificial Intelligence. MoChArt 2006. Lecture Notes in Computer Science(), vol 4428. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74128-2_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-74128-2_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74127-5
Online ISBN: 978-3-540-74128-2
eBook Packages: Computer ScienceComputer Science (R0)