Abstract
To verify the correctness of Java programs, a novel approach for model checking Java programs with MSVL (Modeling, Simulation and Verification Language) is advocated. To this end, the rules for decoding the object-oriented semantics of Java Language with the process-oriented semantics of MSVL are defined, and the technique for automatically rewriting a Java 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 Java programs in a direct way, and helps to improve the quality of the software system.
This research is partly supported by the Industrial Research Project of Shaanxi Province No. 2017GY-076, No. 2016GY-123, and the NSFC Grant No. 61672403.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Arnold, K., Gosling, J., Holmes, D.: Java Programming Language, 4th edn. Addison-Wesley Professional, Boston (2005)
Clarke, E.M.: Model checking. Lect. Notes Comput. Sci. 164(2), 305–349 (1999)
Holzmann, J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)
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)
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_17
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_42
Brat, G., Havelund, K., Visser, W.: Java pathfinder-second generation of a Java model checker (2000)
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_7
Duan, Z., Yang, X., Koutny, M.: Framed temporal logic programming. Sci. Comput. Program. 70(1), 31–61 (2008)
Duan, Z.: Temporal logic and temporal logic programming. Science Press (2005)
Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Informatica 45(1), 43–78 (2008)
Zhang, N., Duan, Z., Tian, C.: A cylinder computation model for many-core parallel computing. Theoret. Comput. Sci. 497, 68–83 (2013)
Tian, C., Duan, Z., Duan, Z.: Making CEGAR more efficient in software model checking. IEEE Trans. Softw. Eng. 40(12), 1206–1223 (2014)
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)
Duan, Z., Tian, C.: A practical decision procedure for propositional projection temporal logic with infinite models. Theoret. Comput. Sci. 554, 169–190 (2014)
Tian, C., Duan, Z., Zhang, N.: An efficient approach for abstraction-refinement in model checking. Theoret. Comput. Sci. 461, 76–85 (2012)
Duan, Z.: Modeling and analysis of hybrid systems. Science Press (2004)
Wang, M., Duan, Z., Tian, C.: Simulation and verification of the virtual memory management system with MSVL. In: CSCWD 2014, pp. 360–365 (2014)
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_8
Wang, X., Tian, C., Duan, Z., Zhao, L.: MSVL: a typed language for temporal logic programming. Front. Comput. Sci. 5, 762–785 (2017)
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_48
Zhang, N., Duan, Z., Tian, C.: A mechanism of function calls in MSVL. Theoret. Comput. Sci. 654, 11–25 (2016)
Tian, C., Duan, Z.: Expressiveness of propositional projection temporal logic with star. Theoret. Comput. Sci. 412(18), 1729–1744 (2011)
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_12
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_13
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Shu, X., Luo, N., Wang, B., Wang, X., Zhao, L. (2019). Model Checking Java Programs with MSVL. In: Duan, Z., Liu, S., Tian, C., Nagoya, F. (eds) Structured Object-Oriented Formal Language and Method. SOFL+MSVL 2018. Lecture Notes in Computer Science(), vol 11392. Springer, Cham. https://doi.org/10.1007/978-3-030-13651-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-13651-2_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-13650-5
Online ISBN: 978-3-030-13651-2
eBook Packages: Computer ScienceComputer Science (R0)