Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2016 | OriginalPaper | Buchkapitel

1. Automatic Refinement Checking for Formal System Models

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

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

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

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.

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
Nächstes Kapitel Towards Simulation Based Evaluation of Safety Goal Violations in Automotive Systems
Fußnoten
1
The post-condition is a binary predicate, since it can also depend on the source state, which is expressed using @pre in OCL.
 
2
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.
 
Literatur
1.
Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)CrossRefMATH
2.
Abrial, J.R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York (2010)CrossRefMATH
3.
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)
4.
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
5.
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
6.
Boiten, E.A.: Introducing extra operations in refinement. In: Formal Aspects of Computing, Springer London, pp. 1–13. Springer, London (2012)
7.
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
8.
Briand, L.C., Labiche, Y., Yue, T.: Automated traceability analysis for uml model refinements. Inf. Softw. Technol. 51, 512–527 (2009)CrossRef
9.
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
Metadaten
Titel
Automatic Refinement Checking for Formal System Models
verfasst von
Julia Seiter
Robert Wille
Ulrich Kühne
Rolf Drechsler
Copyright-Jahr
2016
Buch
Languages, Design Methods, and Tools for Electronic System Design

Print ISBN: 978-3-319-24455-6

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

Copyright-Jahr: 2016

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

Neuer Inhalt

    Bildnachweise