Advertisement

A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis

  • Piergiorgio Bertoli
  • Marco Bozzano
  • Alessandro Cimatti
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4428)

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.

Keywords

Model Check Safety Analysis Linear Temporal Logic Kripke Structure Computation Tree Logic 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Å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)Google Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    Bertoli, P., Cimatti, A., Pistore, M.: Strong Cyclic Planning under Partial Observability. In: Proc. of 17th European Conference on Artificial Intelligence (ECAI 2006) (2006)Google Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    Bertoli, P., Cimatti, A., Roveri, M., Traverso, P.: Strong Planning under Partial Observability. Artificial Intelligence 170, 337–384 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    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)CrossRefGoogle Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    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)Google Scholar
  11. 11.
    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, 2003Google Scholar
  12. 12.
    Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)CrossRefGoogle Scholar
  13. 13.
    Bryant, R.E.: Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams. ACM Computing Surveys 24(3), 293–318 (1992)CrossRefGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    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)zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    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)zbMATHMathSciNetGoogle Scholar
  19. 19.
    Cimatti, A., Roveri, M., Bertoli, P.: Conformant Planning via Symbolic Model Checking and Heuristic Search. Artificial Intelligence 159, 127–206 (2004)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    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)Google Scholar
  21. 21.
    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)CrossRefGoogle Scholar
  22. 22.
    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)zbMATHCrossRefGoogle Scholar
  23. 23.
    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)Google Scholar
  24. 24.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge, MA (1999)Google Scholar
  25. 25.
    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)Google Scholar
  26. 26.
    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)Google Scholar
  27. 27.
    Coudert, O., Madre, J.C.: Fault Tree Analysis: 1020 Prime Implicants and Beyond. In: Proc. Annual Reliability and Maintainability Symposium (RAMS 1993) (1993)Google Scholar
  28. 28.
    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)Google Scholar
  29. 29.
    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)CrossRefGoogle Scholar
  30. 30.
    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)Google Scholar
  31. 31.
    Emerson, E.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, vol. B, Formal Models and Semantics, Elsevier, Amsterdam (1990)Google Scholar
  32. 32.
    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)CrossRefGoogle Scholar
  33. 33.
    The FSAP platform. http://sra.itc.it/tools/FSAP
  34. 34.
    Ghallab, M., Nau, D., Traverso, P.: Automated Planning: Theory and Practice. 1, pp. 17–110. Morgan Kaufmann, Washington (2004)zbMATHCrossRefGoogle Scholar
  35. 35.
    Gupta, A., Clarke, E., Strichman, O.: Sat based counterexample-guided abstraction-refinement. IEEE Transactions on Computer Aided Design 23, 1113–1123 (2004)CrossRefGoogle Scholar
  36. 36.
    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)Google Scholar
  37. 37.
    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)Google Scholar
  38. 38.
    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)MathSciNetGoogle Scholar
  39. 39.
    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)zbMATHCrossRefMathSciNetGoogle Scholar
  40. 40.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)zbMATHGoogle Scholar
  41. 41.
    The NuSMV model checker, http://nusmv.itc.it
  42. 42.
    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)Google Scholar
  43. 43.
    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)Google Scholar
  44. 44.
    Prasad, M., Biere, A., Gupta, A.: A survey of recent advances in sat-based formal verification. STTT (7), 156–173 (2005)CrossRefGoogle Scholar
  45. 45.
    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)Google Scholar
  46. 46.
    Rauzy, A.: New Algorithms for Fault Trees Analysis. Reliability Engineering and System Safety 40(3), 203–211 (1993)CrossRefGoogle Scholar
  47. 47.
    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)Google Scholar
  48. 48.
    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)zbMATHCrossRefMathSciNetGoogle Scholar
  49. 49.
    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)CrossRefGoogle Scholar
  50. 50.
    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)CrossRefGoogle Scholar
  51. 51.
    Siu, N.O.: Risk Assessment for Dynamic Systems: An Overview. Reliability Engineering and System Safety 43, 43–74 (1994)CrossRefGoogle Scholar
  52. 52.
    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)Google Scholar
  53. 53.
    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)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Piergiorgio Bertoli
    • 1
  • Marco Bozzano
    • 1
  • Alessandro Cimatti
    • 1
  1. 1.ITC-irst - Via Sommarive 18 - 38050 Povo - TrentoItaly

Personalised recommendations