×

zbMATH — the first resource for mathematics

A mechanism of function calls in MSVL. (English) Zbl 1353.68184
Summary: Modeling, Simulation and Verification Language (MSVL) is a useful formalism for specification and verification of concurrent systems. To make it more practical and easier to use, we extend MSVL with external and internal function calls. To do so, the syntax of function definitions and function calls is formalized. Then, the syntax of expressions in MSVL is extended by including function calls. Further, the evaluation rules are redefined. Moreover, the set of statements in MSVL is also extended and the semantics of function call statements is formalized. In addition, the existence of minimal models of MSVL programs involving new added statements is proved. Finally, an example is given to illustrate how to interpret function calls in practice with MSVL.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N17 Logic programming
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
CESAR
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Floyd, R. W., The paradigms of programming, Commun. ACM, 22, 8, 455-460, (1979)
[2] Cox, B., Object oriented programming, (1985), Addison-Wesley Reading, MA
[3] Sillitti, A.; Vernazza, T.; Succi, G., Service oriented programming: a new paradigm of software reuse, (Proceedings of the 7th International Conference on Software Reuse: Methods, Techniques, and Tools, ICSR-7, (2002), Springer-Verlag), 269-280 · Zbl 1051.68807
[4] Grumberg, O.; Long, D. E., Model checking and modular verification, ACM Trans. Program. Lang. Syst., 16, 3, 843-871, (1994)
[5] Berezin, S.; Campos, S. V.A.; Clarke, E. M., Compositional reasoning in model checking, (Revised Lectures from the International Symposium on Compositionality: The Significant Difference, COMPOS’97, (1998), Springer-Verlag), 81-102
[6] Alur, R.; Henzinger, T., Modularity for timed and hybrid systems, (Concurrency Theory, CONCUR ’97, Lecture Notes in Computer Science, vol. 1243, (1997), Springer Berlin, Heidelberg), 74-88
[7] Duan, Z., Temporal logic and temporal logic programming, (2005), Science Press Beijing
[8] Han, M.; Duan, Z.; Wang, X., Time constraints with temporal logic programming, (Formal Methods and Software Engineering - Proceedings of 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, (2012)), 266-282
[9] Manna, Z.; Pnueli, A., The temporal logic of reactive and concurrent system, (1992), Springer-Verlag New York
[10] Pnueli, A., The temporal logic of programs, (18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October-1 November, (1977)), 46-57
[11] Queille, J.; Sifakis, J., Specification and verification of concurrent systems in CESAR, (Proceedings of International Symposium on Programming, 5th Colloquium, Torino, Italy, April 6-8, (1982)), 337-351 · Zbl 0482.68028
[12] Zhang, N.; Duan, Z.; Tian, C.; Du, D., A formal proof of the deadline driven scheduler in PPTL axiomatic system, Theoret. Comput. Sci., 554, 229-253, (2014) · Zbl 1360.68771
[13] Liu, C. L.; Layland, J. W., Scheduling algorithms for multiprogramming in a hard-real-time environment, J. ACM, 20, 1, 46-61, (1973) · Zbl 0265.68013
[14] Zhang, N.; Duan, Z.; Tian, C., A cylinder computation model for many-core parallel computing, Theoret. Comput. Sci., 497, 68-83, (2013) · Zbl 1416.68074
[15] Mo, D.; Wang, X.; Duan, Z., Asynchronous communication in MSVL, (Formal Methods and Software Engineering - Proceedings of 13th International Conference on Formal Engineering Methods, ICFEM 2011, Durham, UK, October 26-28, (2011)), 82-97
[16] Wang, X.; Duan, Z.; Zhao, L., Formalizing and implementing types in MSVL, (Structured Object-Oriented Formal Language and Method - Third International Workshop, SOFL+MSVL 2013, Queenstown, New Zealand, October 29, (2013)), 62-75, Revised selected papers
[17] Clarke, E. M.; Long, D. E.; McMillan, K. L., Compositional model checking, (Proceedings of the Fourth Annual Symposium on Logic in Computer Science, LICS ’89, Pacific Grove, California, USA, June 5-8, (1989)), 353-362 · Zbl 0716.68035
[18] Moszkowski, B., Executing temporal logic programs, (1986), Cambridge University Press Cambridge · Zbl 0658.68014
[19] Duan, Z.; Yang, X.; Koutny, M., Framed temporal logic programming, Sci. Comput. Program., 70, 1, 31-61, (2008) · Zbl 1131.68036
[20] Qin, S.; He, G.; Luo, C.; Chin, W.; Yang, H., Automatically refining partial specifications for heap-manipulating programs, Sci. Comput. Program., 82, 56-76, (2014)
[21] Bidoit, N., Negation in rule-based database languages: a survey, (Selected Papers of the Workshop on Deductive Database Theory, (1991), Elsevier Science Publishers B. V. Amsterdam, The Netherlands), 3-83 · Zbl 0716.68025
[22] McMillan, K. L., A methodology for hardware verification using compositional model checking, Sci. Comput. Program., 37, 1-3, 279-309, (2000) · Zbl 0954.68005
[23] Chaki, S.; Clarke, E.; Groce, A.; Jha, S.; Veith, H., Modular verification of software components in C, (Proceedings of the 25th International Conference on Software Engineering, ICSE ’03, (2003)), 385-395
[24] Fisler, K.; Krishnamurthi, S., Modular verification of collaboration-based software designs, SIGSOFT Softw. Eng. Notes, 26, 5, 152-163, (2001)
[25] Hailpern, B.; Owicki, S., Modular verification of computer communication protocols, IEEE Trans. Commun., 31, 1, 56-68, (1983)
[26] Flanagan, C.; Freund, S. N.; Qadeer, S.; Seshia, S. A., Modular verification of multithreaded programs, Theoret. Comput. Sci., 338, 1-3, 153-183, (2005) · Zbl 1108.68080
[27] Tang, C., Toward a unified logic basis for programming languages, (Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, (1983)), 425-429
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.