nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Model Checking Java Programs with MSVL

verfasst von : Xinfeng Shu, Na Luo, Bo Wang, Xiaobing Wang, Liang Zhao

Erschienen in: Structured Object-Oriented Formal Language and Method

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Verification of SysML Activity Diagrams Using Hoare Logic and SOFL

Nächstes Kapitel Formal Specification and Verification for Real-Time Scheduling Based on PAR

Arnold, K., Gosling, J., Holmes, D.: Java Programming Language, 4th edn. Addison-Wesley Professional, Boston (2005)MATH

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.

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

12.

Duan, Z.: Temporal logic and temporal logic programming. Science Press (2005)

13.

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

14.

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

15.

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

16.

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

17.

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

18.

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

19.

Duan, Z.: Modeling and analysis of hybrid systems. Science Press (2004)

20.

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

21.

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

22.

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

23.

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

24.

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

25.

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

26.

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

27.

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

Titel: Model Checking Java Programs with MSVL
verfasst von: Xinfeng Shu
Na Luo
Bo Wang
Xiaobing Wang
Liang Zhao
Verlag: Springer International Publishing
Buch: Structured Object-Oriented Formal Language and Method
Print ISBN: 978-3-030-13650-5

Electronic ISBN: 978-3-030-13651-2

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-13651-2_6

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner