Top

Published in:

2016 | OriginalPaper | Chapter

1. Automatic Refinement Checking for Formal System Models

Authors : Julia Seiter, Robert Wille, Ulrich Kühne, Rolf Drechsler

Published in: Languages, Design Methods, and Tools for Electronic System Design

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

For the design of complex systems, formal modelling languages such as UML or SysML find significant attention. The typical model-driven design flow assumes thereby an initial (abstract) model which is iteratively refined to a more precise description. During this process, new errors and inconsistencies might be introduced. In this chapter, we propose an automatic method for verifying the consistency of refinements in UML or SysML. For this purpose, a theoretical foundation is considered from which the corresponding proof obligations are determined. Afterwards, they are encoded as an instance of satisfiability modulo theories (SMT) and solved using proper solving engines. The practical use of the proposed method is demonstrated and compared to a previously proposed approach.

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

next chapter Towards Simulation Based Evaluation of Safety Goal Violations in Automotive Systems

The post-condition is a binary predicate, since it can also depend on the source state, which is expressed using @pre in OCL.

This restriction is common in many approaches (e.g. [3, 11, 12, 30, 31]) and also justified by the fact that, eventually, the implemented system will be realized by bounded physical devices anyway.

Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)CrossRefMATH

Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)CrossRefMATH

Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: A challenging model transformation. In: International Conference on Model Driven Engineering Languages and Systems, pp. 436–450. Springer, New York (2007)

Antoniol, G., Canfora, G., Casazza, G., Lucia, A.D., Merlo, E.: Recovering traceability links between code and documentation. IEEE Trans. Softw. Eng. 28, 970–983 (2002)CrossRef

Ben Ammar, B., Bhiri, M.T., Souquières, J.: Incremental development of UML specifications using operation refinements. Innov. Syst. Softw. Eng. 4(3), 259–266 (2008). doi:10.1007/s11334-008-0056-1CrossRef

Boiten, E.A.: Introducing extra operations in refinement. In: Formal Aspects of Computing, Springer London, pp. 1–13. Springer, London (2012)

Braunstein, C., Encrenaz, E.: CTL-property transformations along an incremental design process. Int. J. Softw. Tools Technol. Transfer 9(1), 77–88 (2006). doi:10.1007/s10009-006-0007-9CrossRefMATH

Briand, L.C., Labiche, Y., Yue, T.: Automated traceability analysis for uml model refinements. Inf. Softw. Technol. 51, 512–527 (2009)CrossRef

Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Tools and Algorithms for Construction and Analysis of Systems, pp. 174–177. Springer, Berlin (2009)

10.

Bulychev, P., Konnov, I.V., Zakharov, V.A.: Computing (bi)simulation relations preserving CTL _X ^∗ for ordinary and fair kripke structures. In: 3ematical Methods and Algorithms, vol. 12, pp. 59–76. Institute for System Programming, Russian Academy of Science (2006)

11.

Cabot, J., Clarisó, R., Riera, D.: Verification of UML/OCL class diagrams using constraint programming. In: IEEE International Conference on Software Testing Verification and Validation Workshop, pp. 73–80 (2008)

12.

Cadoli, M., Calvanese, D., Giacomo, G.D., Mancini, T.: Finite Model Reasoning on UML Class Diagrams Via Constraint Programming. In: R. Basili, M.T. Pazienza (eds.) AI*IA. Lecture Notes in Computer Science, vol. 4733, pp. 36–47. Springer, Berlin (2007)

13.

De Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, pp. 337–340. Springer, Berlin/Heidelberg (2008). URL http://dl.acm.org/citation.cfm?id=1792734.1792766

14.

Derrick, J., Smith, G.: Using model checking to automatically find retrieve relations. Electron. Notes Theor. Comput. Sci. 201, 155–175 (2008)CrossRef

15.

Egyed, A.: Consistent adaptation and evolution of class diagrams during refinement. In: Fundamental Approaches to Software Engineering (2004)CrossRef

16.

Glabbeek, R.: The linear time - branching time spectrum. In: J. Baeten, J. Klop (eds.) CONCUR ’90 Theories of Concurrency: Unification and Extension. Lecture Notes in Computer Science, vol. 458, pp. 278–297. Springer, Berlin/Heidelberg (1990)CrossRef

17.

Gogolla, M., Kuhlmann, M., Hamann, L.: Consistency, independence and consequences in UML and OCL models. In: Tests and Proofs, pp. 90–104. Springer, Berlin (2009)

18.

Goldsmith, M., Roscoe, B., Armstrong, P.: Failures-Divergence Refinement - FDR2 User Manual (2005)

19.

Hayes, J.H., Dekhtyar, A., Osborne, J.: Improving requirements tracing via information retrieval. In: IEEE International Requirements Engineering Conference (2003)CrossRef

20.

Leuschel, M., Butler, M.: Automatic Refinement Checking for B. In: International Conference on Formal Engineering Methods (2005)CrossRefMATH

21.

Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S., Probst, D.: Property preserving abstractions for the verification of concurrent systems. Form. Method. Syst. Des. 6(1), 11–44 (1995)CrossRefMATH

22.

Natt och Dag, J., Regnell, B., Carlshamre, P., Andersson, M., Karlsson, J.: A feasibility study of automated natural language requirements analysis in market-driven development. Requir. Eng. 7, 20–33 (2002)

23.

Nejati, S., Gurfinkel, A., Chechik, M.: Stuttering abstraction for model checking. In: Software Engineering and Formal Methods, pp. 311–320. Springer, Berlin (2005)

24.

Pons, C., Garcia, D.: Practical verification strategy for refinement conditions in UML models. In: Advanced Software Engineering: Expanding the Frontiers of Software Technology. IFIP International Federation for Information Processing, vol. 219, pp. 47–61. Springer, Berlin (2006)

25.

Ranzato, F., Tapparo, F.: Computing stuttering simulations. In: Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 5710, pp. 542–556. Springer, Berlin (2009)

26.

Robinson, N.J.: Finding abstraction relations for data refinement. Technical Report, Software Verification Research Center, The University of Queensland (2003)

27.

Robinson, N.J.: Incremental derivation of abstraction relations for data refinement. In: Formal Methods and Software Engineering. IEEE Computer Society, Los Alamitos (2003)CrossRef

28.

Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language reference manual. Addison-Wesley Longman, Essex (1999)

29.

Snook, C., Butler, M.: UML-B: formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92–122 (2006)CrossRef

30.

Soeken, M., Wille, R., Kuhlmann, M., Gogolla, M., Drechsler, R.: Verifying UML/OCL models using Boolean satisfiability. In: Design, Automation and Test in Europe, pp. 1341–1344. IEEE Computer Society, New York (2010)

31.

Soeken, M., Wille, R., Drechsler, R.: Verifying dynamic aspects of UML models. In: Design, Automation & Test in Europe Conference & Exhibition (DATE), pp. 1–6 (2011)

32.

Warmer, J., Kleppe, A.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley Longman, Boston, MA (1999)

33.

Weilkiens, T.: Systems Engineering with SysML/UML: Modeling, Analysis, Design. Morgan Kaufmann, San Francisco, CA (2008)MATH

34.

Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Upper Saddle River, NJ (1996)MATH

Title: Automatic Refinement Checking for Formal System Models
Authors: Julia Seiter
Robert Wille
Ulrich Kühne
Rolf Drechsler
Publisher: Springer International Publishing
Book: Languages, Design Methods, and Tools for Electronic System Design
Print ISBN: 978-3-319-24455-6

Electronic ISBN: 978-3-319-24457-0

Copyright Year: 2016
DOI: https://doi.org/10.1007/978-3-319-24457-0_1