nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Extending UML for Model Checking

verfasst von : Xinfeng Shu, Mengnan Wang, Xiaobing Wang

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 solve the problem that UML (Unified Modeling Language) design model cannot be model-checked for its rough semantics, an extension of UML, called xUML4MC, is defined by extending the activity diagram with accurate syntax and semantics to model the activities of an object. Besides, the technique for automatical transformation of xUML4MC model into MSVL (Modeling, Simulation and Verification Language) model is also presented, which in turn can be verified with model checking tool MSV. The formalism arms the classical visual specification language UML with the power of model checking, and helps to promote the quality of 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 The Complexity of Linear-Time Temporal Logic Model Repair

Nächstes Kapitel Foundation of a Framework to Support Compliance Checking in Construction Industry

Object Management Group: OMG Unified Modeling Language (OMG UML), Version 2.5 (2015). http://www.omg.org/spec/UML/2.5

ISO/IEC 19501:2005 - Information Technology - Open Distributed Processing - Unified Modeling Language (UML) Version 1.4.2, Iso.org., 01 April 2005. Accessed 07 May 2015

Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. In: Nato Advanced Study Institute on Deductive Program Design, pp. 305–349 (1996)CrossRef

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

Duan, Z., Koutny, M.: A framed temporal logic programming language. J. Comput. Sci. Technol. 19, 333–344 (2004)MathSciNet

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

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

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

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

10.

Wang, X., Tian, C., Duan, Z., Zhao, L.: MSVL: a typed language for temporal logic programming. Front. Comput. Sci. (2017). https://doi.org/10.1007/s11704-016-6059-4

11.

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

12.

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

13.

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

14.

Duan, Z.: Modeling and Analysis of Hybrid Systems. Science Press, Beijing (2004). https://doi.org/10.1007/3-540-45426-8CrossRef

15.

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

16.

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

17.

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

18.

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

19.

Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. China Machine Press, Beijing (2006)

20.

Object Management Group (OMG): Object Constraint Language OMG Available Specification, Version 2.0, May 2006

21.

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

22.

Muram, F.U., Tran, H., Zdun, U.: A model checking based approach for containment checking of UML sequence diagrams. In: Software Engineering Conference, pp. 73–80. IEEE (2017)

23.

Lima, V., Talhi, C., Mouheb, D., et al.: Formal verification and validation of UML 2.0 sequence diagrams using source and destination of messages. Electron. Notes Theoret. Comput. Sci. 254, 143–160 (2009)CrossRef

24.

Gnesi, S., Mazzanti, F.: On the fly model checking of communicating UML State Machines. Acis IEEE, vol. 144, pp. 331–338 (2004)

25.

Mullins, J., Oarga, R.: Model checking of extended OCL constraints on UML models in SOCLe. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 59–75. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72952-5_4CrossRef

Titel: Extending UML for Model Checking
verfasst von: Xinfeng Shu
Mengnan Wang
Xiaobing Wang
Verlag: Springer International Publishing
Buch: Structured Object-Oriented Formal Language and Method
Print ISBN: 978-3-319-90103-9

Electronic ISBN: 978-3-319-90104-6

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-90104-6_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"