Automatic refinement checking for formal system models

Julia Seiter; Robert Wille; Ulrich Kühne; Rolf Drechsler

doi:10.1007/978-3-319-24457-0_1

Automatic refinement checking for formal system models

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

University of Bremen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Languages, Design Methods, and Tools for Electronic System Design - Selected Contributions from FDL 2014
Editors	Frank Oppenheimer, Julio Luis Medina Pasaje
Publisher	Springer Verlag
Pages	3-22
Number of pages	20
ISBN (Print)	9783319244556
DOIs	https://doi.org/10.1007/978-3-319-24457-0_1
State	Published - 2016
Externally published	Yes
Event	16th Conference on Languages, Design Methods, and Tools for Electronic System Design, FDL 2014 - Munich, Germany Duration: 14 Oct 2014 → 16 Oct 2014

Publication series

Name	Lecture Notes in Electrical Engineering
Volume	361
ISSN (Print)	1876-1100
ISSN (Electronic)	1876-1119

Conference

Conference	16th Conference on Languages, Design Methods, and Tools for Electronic System Design, FDL 2014
Country/Territory	Germany
City	Munich
Period	14/10/14 → 16/10/14

Access to Document

10.1007/978-3-319-24457-0_1

Cite this

Seiter, J., Wille, R., Kühne, U., & Drechsler, R. (2016). Automatic refinement checking for formal system models. In F. Oppenheimer, & J. L. M. Pasaje (Eds.), Languages, Design Methods, and Tools for Electronic System Design - Selected Contributions from FDL 2014 (pp. 3-22). (Lecture Notes in Electrical Engineering; Vol. 361). Springer Verlag. https://doi.org/10.1007/978-3-319-24457-0_1

@inproceedings{f853861926b741d3b04285fa3ddacaca,

title = "Automatic refinement checking for formal system models",

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.",

author = "Julia Seiter and Robert Wille and Ulrich K{\"u}hne and Rolf Drechsler",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2016; 16th Conference on Languages, Design Methods, and Tools for Electronic System Design, FDL 2014 ; Conference date: 14-10-2014 Through 16-10-2014",

year = "2016",

doi = "10.1007/978-3-319-24457-0_1",

language = "English",

isbn = "9783319244556",

series = "Lecture Notes in Electrical Engineering",

publisher = "Springer Verlag",

pages = "3--22",

editor = "Frank Oppenheimer and Pasaje, {Julio Luis Medina}",

booktitle = "Languages, Design Methods, and Tools for Electronic System Design - Selected Contributions from FDL 2014",

}

Seiter, J, Wille, R, Kühne, U & Drechsler, R 2016, Automatic refinement checking for formal system models. in F Oppenheimer & JLM Pasaje (eds), Languages, Design Methods, and Tools for Electronic System Design - Selected Contributions from FDL 2014. Lecture Notes in Electrical Engineering, vol. 361, Springer Verlag, pp. 3-22, 16th Conference on Languages, Design Methods, and Tools for Electronic System Design, FDL 2014, Munich, Germany, 14/10/14. https://doi.org/10.1007/978-3-319-24457-0_1

Automatic refinement checking for formal system models. / Seiter, Julia; Wille, Robert; Kühne, Ulrich et al.
Languages, Design Methods, and Tools for Electronic System Design - Selected Contributions from FDL 2014. ed. / Frank Oppenheimer; Julio Luis Medina Pasaje. Springer Verlag, 2016. p. 3-22 (Lecture Notes in Electrical Engineering; Vol. 361).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Automatic refinement checking for formal system models

AU - Seiter, Julia

AU - Wille, Robert

AU - Kühne, Ulrich

AU - Drechsler, Rolf

N1 - Publisher Copyright: © Springer International Publishing Switzerland 2016

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84952774724&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-24457-0_1

DO - 10.1007/978-3-319-24457-0_1

M3 - Conference contribution

AN - SCOPUS:84952774724

SN - 9783319244556

T3 - Lecture Notes in Electrical Engineering

SP - 3

EP - 22

BT - Languages, Design Methods, and Tools for Electronic System Design - Selected Contributions from FDL 2014

A2 - Oppenheimer, Frank

A2 - Pasaje, Julio Luis Medina

PB - Springer Verlag

T2 - 16th Conference on Languages, Design Methods, and Tools for Electronic System Design, FDL 2014

Y2 - 14 October 2014 through 16 October 2014

ER -

Automatic refinement checking for formal system models

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this