×

zbMATH — the first resource for mathematics

Modeling for verification. (English) Zbl 1392.68264
Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 75-105 (2018).
Summary: System modeling is the initial, and often crucial, step in verification. The right choice of model and modeling language is important for both designers and users of verification tools. This chapter aims to provide a guide to system modeling in four stages. First, it provides an overview of the main issues one must consider in modeling systems for verification. These issues involve both the selection or design of a modeling language and the steps of model creation. Next, it introduces a simple modeling language, sml, for illustrating the issues involved in selecting or designing a modeling language. sml uses an abstract state machine formalism that captures key features of widely-used languages based on transition system representations. We introduce the simple modeling language to simplify the connection between languages used by practitioners (such as Verilog, Simulink, or C) and various underlying formalisms (e.g., automata or Kripke structures) used in model checking. Third, the chapter demonstrates key steps in model creation using sml with illustrative examples. Finally, the presented modeling language sml is mapped to standard formalisms such as Kripke structures.
For the entire collection see [Zbl 1390.68001].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 1. Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117-126 (1987) · Zbl 0641.68039
[2] 2. Alur, R., Courcoubetis, C., Dill, D.: Model checking in dense real time. Inf. Comput. 104(1), 2-34 (1993) · Zbl 0783.68076
[3] 3. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138, 3-34 (1995) · Zbl 0874.68206
[4] 4. Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126, 183-235 (1994) · Zbl 0803.68071
[5] 5. Alur, R., Henzinger, T.: Logics and models of real time: a survey. In: Real Time: Theory in Practice. LNCS, vol. 600 (1992)
[6] 6. Alur, R., Henzinger, T.: Reactive modules. Form. Methods Syst. Des. 15, 7-48 (1999)
[7] 7. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76-85 (2010)
[8] 8. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P., Siegle, M. (eds.): Validation of Stochastic Systems—A Guide to Current Research. LNCS, vol. 2925. Springer, Heidelberg (2004) · Zbl 1047.68001
[9] 9. Baier, C., Majster-Cederbaum, M.: Denotational semantics in the CPO and metric approach. Theor. Comput. Sci. 135(2), 171-220 (1994) · Zbl 0829.68079
[10] 10. Balarin, F., Watanabe, Y., Hsieh, H., Lavagno, L., Passerone, R., Sangiovanni-Vincentelli, A.: Metropolis: an integrated electronic system design environment. IEEE Comput. 36, 45-52 (2003)
[11] 11. Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 4. IOS Press, Amsterdam (2009). Chap. 8
[12] 12. Behrmann, G., Larsen, K., Rasmussen, J.: Priced timed automata: algorithms and applications. In: Third International Symposium on Formal Methods for Components and Objects (FMCO), pp. 162-182 (2004) · Zbl 1143.68430
[13] 13. Benveniste, A., Caspi, P., Lublinerman, R., Tripakis, S.: Actors without directors: a Kahnian view of heterogeneous systems. In: HSCC’09: Proceedings of the 12th International Conference on Hybrid Systems: Computation and Control. LNCS, pp. 46-60. Springer, Heidelberg (2009). doi: · Zbl 1237.68122
[14] 14. Berry, G., Gonthier, G.: The Esterel synchronous programming language: design, semantics, implementation. Sci. Comput. Program. 19(2), 87-152 (1992) · Zbl 0772.68013
[15] 15. Brady, B., Bryant, R., Seshia, S.: Abstracting RTL designs to the term level. Tech. Rep. UCB/EECS-2008-136, EECS Department, University of California, Berkeley (2008)
[16] 16. Brady, B., Bryant, R., Seshia, S., O’Leary, J.: ATLAS: automatic term-level abstraction of RTL designs. In: Proceedings of the Eighth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE) (2010)
[17] 17. Broman, D., Lee, E., Tripakis, S., Törngren, M.: Viewpoints, formalisms, languages, and tools for cyber-physical systems. In: 6th International Workshop on Multi-paradigm Modeling (MPM’12) (2012)
[18] 18. Broy, M., Stolen, K.: Specification and Development of Interactive Systems. Monographs in Computer Science, vol. 62. Springer, Heidelberg (2001) · Zbl 0981.68115
[19] 19. Bryant, R.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35(8), 677-691 (1986) · Zbl 0593.94022
[20] 20. Bryant, R., Lahiri, S., Seshia, S.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K. (eds.) Proc. Computer-Aided Verification (CAV’02). LNCS, vol. 2404, pp. 78-92 (2002) · Zbl 1010.68522
[21] 21. Buck, J.: Scheduling dynamic dataflow graphs with bounded memory using the token flow model. Ph.D. thesis, University of California, Berkeley (1993)
[22] 22. Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: Lustre: a declarative language for programming synchronous systems. In: 14th ACM Symp. POPL. ACM, New York (1987)
[23] 23. Chatterjee, K., Doyen, L., Henzinger, T.: Quantitative languages. In: Proc. Computer Science Logic (CSL). LNCS, vol. 5213, pp. 385-400 (2008) · Zbl 1156.68449
[24] 24. Chatterjee, K., Doyen, L., Henzinger, T.: Alternating weighted automata. In: Fundamentals of Computation Theory (FCT). LNCS, vol. 5699, pp. 3-13 (2009) · Zbl 1252.68167
[25] 25. Clarke, E., Grumberg, O., Peled, D. (eds.): Model Checking. MIT Press, Cambridge (2001) · Zbl 0847.68063
[26] 26. Commoner, F., Holt, A.W., Even, S., Pnueli, A.: Marked directed graphs. J. Comput. Syst. Sci. 5, 511-523 (1971) · Zbl 0238.05109
[27] 27. Cruz, R.L.: A calculus for network delay, part I. Network elements in isolation. IEEE Trans. Inf. Theory 37(1), 114-131 (1991) · Zbl 0712.94028
[28] 28. Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. Form. Methods Syst. Des. 19(1), 45-80 (2001) · Zbl 0985.68033
[29] 29. Davare, A., Densmore, D., Meyerowitz, T., Pinto, A., Sangiovanni-Vincentelli, A., Yang, G., Zeng, H., Zhu, Q.: A next-generation design framework for platform-based design. In: Conference on Using Hardware Design and Verification Languages (DVCon), vol. 152 (2007)
[30] 30. Davis, M.: Markov Models and Optimization. Chapman & Hall, London (1993) · Zbl 0780.60002
[31] 31. Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool KRONOS. In: Alur, R., Henzinger, T., Sontag, E. (eds.) Hybrid Systems III: Verification and Control. LNCS, vol. 1066, pp. 208-219. Springer, Heidelberg (1996)
[32] 32. Eker, J., Janneck, J., Lee, E., Liu, J., Liu, X., Ludvig, J., Neuendorffer, S., Sachs, S., Xiong, Y.: Taming heterogeneity—the Ptolemy approach. Proc. IEEE 91(1), 127-144 (2003)
[33] 33. Fokkink, W.: Introduction to Process Algebra. Springer, Heidelberg (2000) · Zbl 0941.68087
[34] 34. Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.): Abstract State Machines, Theory and Applications, Proceedings of the International Workshop, ASM 2000, Monte Verità, Switzerland, March 19-24, 2000. LNCS, vol. 1912. Springer, Heidelberg (2000) · Zbl 0947.00040
[35] 35. Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8, 231-274 (1987) · Zbl 0637.68010
[36] 36. Hoare, C.: Communicating Sequential Processes. Prentice Hall, New York (1985) · Zbl 0637.68007
[37] 37. Holcomb, D., Brady, B., Seshia, S.: Abstraction-based performance analysis of NoCs. In: Proceedings of the Design Automation Conference (DAC), pp. 492-497 (2011)
[38] 38. Hopcroft, J., Motwani, R., Ullman, J.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Addison-Wesley, Reading (2006) · Zbl 0980.68066
[39] 39. Hu, J., Lygeros, J., Sastry, S.: Towards a theory of stochastic hybrid systems. In: Hybrid Systems: Computation and Control (HSCC). LNCS, vol. 1790, pp. 160-173. Springer, Heidelberg (2000) · Zbl 0962.93082
[40] 40. ITU: Z.120—Message Sequence Chart (MSC). Available at
[41] 41. ITU: Z.120 Annex B: Formal semantics of Message Sequence Charts. Available at
[42] 42. Kahn, G.: The semantics of a simple language for parallel programming. In: Information Processing 74. Proceedings of IFIP Congress, vol. 74. North-Holland, Amsterdam (1974) · Zbl 0299.68007
[43] 43. Karp, R., Miller, R.: Properties of a model for parallel computations: determinacy, termination, queueing. SIAM J. Appl. Math. 14(6), 1390-1411 (1966) · Zbl 0149.12501
[44] 44. Kohavi, Z.: Switching and Finite Automata Theory, 2nd edn. McGraw-Hill, New York (1978) · Zbl 0384.94020
[45] 45. Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM’07). LNCS, vol. 4486, pp. 220-270. Springer, Heidelberg (2007) · Zbl 1323.68379
[46] 46. Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125-143 (1977) · Zbl 0349.68006
[47] 47. Larsen, K., Petterson, P., Yi, W.: Uppaal in a nutshell. Software Tools for Technology Transfer 1(1/2) (1997) · Zbl 1060.68577
[48] 48. Lee, E., Messerschmitt, D.: Synchronous data flow. Proc. IEEE 75(9), 1235-1245 (1987)
[49] 49. Lee, E., Seshia, S.: Introduction to Embedded Systems—A Cyber-physical Systems Approach (2011) · Zbl 1371.68001
[50] 50. Liu, X., Lee, E.: CPO semantics of timed interactive actor networks. Theor. Comput. Sci. 409(1), 110-125 (2008) · Zbl 1157.68046
[51] 51. Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Commun. ACM 52(8), 76-82 (2009)
[52] 52. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1991) · Zbl 0753.68003
[53] 53. Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980) · Zbl 0452.68027
[54] 54. Milner, R.: Communicating and Mobile Systems: The · Zbl 0942.68002
[55] 55. Peh, L.S.: Flow control and micro-architectural mechanisms for extending the performance of interconnection networks. Ph.D. thesis, Stanford University (2001)
[56] 56. Reisig, W.: Petri Nets: An Introduction. Springer, Heidelberg (1985) · Zbl 0555.68033
[57] 57. Seshia, S.: Quantitative analysis of software: challenges and recent advances. In: 7th International Workshop on Formal Aspects of Component Software (FACS) (2010)
[58] 58. Stergiou, C., Tripakis, S., Matsikoudis, E., Lee, E.: On the verification of timed discrete-event models. In: FORMATS 2013. Springer, Heidelberg (2013) · Zbl 1318.68117
[59] 59. Theelen, B., Geilen, M., Stuijk, S., Gheorghita, S., Basten, T., Voeten, J., Ghamarian, A.: Scenario-aware dataflow. Tech. Rep. ESR-2008-08, Eindhoven University of Technology, (2008)
[60] 60. Tripakis, S.: Compositionality in the science of system design. Proc. IEEE 104(5), 960-972 (2016)
[61] 61. Tripakis, S., Stergiou, C., Shaver, C., Lee, E.: A modular formal semantics for Ptolemy. Math. Struct. Comput. Sci. 23, 834-881 (2013). doi: · Zbl 1271.68238
[62] 62. Yates, R.: Networks of real-time processes. In: Best, E. (ed.) Proc. of the 4th Int. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 715. Springer, Heidelberg (1993)
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.