Top

Published in:

2020 | OriginalPaper | Chapter

Model Checking Python Programs with MSVL

Authors : Xinfeng Shu, Fengyun Gao, Weiran Gao, Lili Zhang, Xiaobing Wang, Liang Zhao

Published in: Structured Object-Oriented Formal Language and Method

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

To verify the correctness of Python programs, a novel approach for model checking Python programs with MSVL (Modeling, Simulation and Verification Language) is advocated. To this end, the rules for decoding the object-oriented semantics of Python with the process-oriented semantics of MSVL are defined, and the technique for automatically rewriting a Python program into its equivalent MSVL program is formalized, which in turn can be verified with the model checking tool MSV. In addition, an example is given to illustrate how the approach works. The approach fully utilizes the powerful expressiveness of MSVL to verify Python programs in a direct way, and helps to improve the quality of the software system.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Formal Specification and Model Checking of a Ride-sharing System in Maude

next chapter Prediction of Function Removal Propagation in Linux Evolution

Sanner, M.F.: Python: a programming language for software integration and development. J. Mol. Graph. Model. 17(1), 57–61 (1999)

Clarke, E.M.: Model checking. Lect. Notes Comput. Sci. 164(2), 305–349 (1999)MATH

Holzmann, J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)CrossRef

Cavada, R., Cimatti, A., Jochim, C.A.: NuSMV 2.5 User Manual. http://nusmv.fbk.eu/ NuSMV/userman/v25/nusmv.pdf

Ball, T., Rajarnani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL 2002, pp. 1–3 (2002)CrossRef

Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44829-2_17CrossRefMATH

Chaki, S., Clarke, E., Groce, A., et al.: Modular verification of software components in C. In: International Conference on Software Engineering, pp. 385–395 (2003)

Cordeiro, L., Morse, J., Nicole, D., Fischer, B.: Context-bounded model checking with ESBMC 1.17. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 534–537. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_42CrossRef

Brat, G., Havelund, K., Visser, W.: Java PathFinder-Second Generation of a Java Model Checker (2000)

10.

Yu, Y., Duan, Z., Tian, C., Yang, M.: Model checking C programs with MSVL. In: Liu, S. (ed.) SOFL 2012. LNCS, vol. 7787, pp. 87–103. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39277-1_7CrossRef

11.

Shu, X., Luo, N., Wang, B., Wang, X., Zhao, L.: Model checking Java programs with MSVL. In: Duan, Z., Liu, S., Tian, C., Nagoya, F. (eds.) SOFL+MSVL 2018. LNCS, vol. 11392, pp. 89–107. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-13651-2_6CrossRef

12.

Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31–61 (2008)MathSciNetCrossRef

13.

Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2005)

14.

Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45(1), 43–78 (2008)MathSciNetCrossRef

15.

Zhang, N., Duan, Z., Tian, C.: A cylinder computation model for many-core parallel computing. Theoret. Comput. Sci. 497, 68–83 (2013)MathSciNetCrossRef

16.

Tian, C., Duan, Z., Duan, Z.: Making CEGAR more efficient in software model checking. IEEE Trans. Softw. Eng. 40(12), 1206–1223 (2014)CrossRef

17.

Zhang, N., Duan, Z., Tian, C.: A complete axiom system for propositional projection temporal logic with cylinder computation model. Theoret. Comput. Sci. 609, 639–657 (2016)MathSciNetCrossRef

18.

Duan, Z., Tian, C.: A practical decision procedure for propositional projection temporal logic with infinite models. Theoret. Comput. Sci. 554, 169–190 (2014)MathSciNetCrossRef

19.

Tian, C., Duan, Z., Zhang, N.: An efficient approach for abstraction-refinement in model checking. Theoret. Comput. Sci. 461, 76–85 (2012)MathSciNetCrossRef

20.

Duan, Z.: Modeling and Analysis of Hybrid Systems. Science Press, Beijing (2004)

21.

Wang, M., Duan, Z., Tian, C.: Simulation and verification of the virtual memory management system with MSVL. In: CSCWD 2014, pp. 360–365 (2014)

22.

Shu, X., Duan, Z.: Model checking process scheduling over multi-core computer system with MSVL. In: Liu, S., Duan, Z. (eds.) SOFL+MSVL 2015. LNCS, vol. 9559, pp. 103–117. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-31220-0_8CrossRef

23.

Wang, X., Tian, C., Duan, Z., Zhao, L.: MSVL: a typed language for temporal logic programming. Front. Comput. Sci. 5, 762–785 (2017)CrossRef

24.

Shu, X., Duan, Z.: Extending MSVL with semaphore. In: Dinh, T.N., Thai, M.T. (eds.) COCOON 2016. LNCS, vol. 9797, pp. 599–610. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42634-1_48CrossRef

25.

Zhang, N., Duan, Z., Tian, C.: A mechanism of function calls in MSVL. Theoret. Comput. Sci. 654, 11–25 (2016)MathSciNetCrossRef

26.

Tian, C., Duan, Z.: Expressiveness of propositional projection temporal logic with star. Theoret. Comput. Sci. 412(18), 1729–1744 (2011)MathSciNetCrossRef

27.

Duan, Z., Tian, C.: A unified model checking approach with projection temporal logic. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 167–186. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88194-0_12CrossRef

28.

Shu, X., Wang, M., Wang, X.: Extending UML for model checking. In: Tian, C., Nagoya, F., Liu, S., Duan, Z. (eds.) SOFL+MSVL 2017. LNCS, vol. 10795, pp. 88–107. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-90104-6_6CrossRef

29.

Shu, X., Li, C., Liu, C.: A Visual modeling language for MSVL. In: Liu, S., Duan, Z., Tian, C., Nagoya, F. (eds.) SOFL+MSVL 2016. LNCS, vol. 10189, pp. 220–237. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57708-1_13CrossRef

Title: Model Checking Python Programs with MSVL
Authors: Xinfeng Shu
Fengyun Gao
Weiran Gao
Lili Zhang
Xiaobing Wang
Liang Zhao
Publisher: Springer International Publishing
Book: Structured Object-Oriented Formal Language and Method
Print ISBN: 978-3-030-41417-7

Electronic ISBN: 978-3-030-41418-4

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-41418-4_15

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner