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

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
titre	Languages, Design Methods, and Tools for Electronic System Design - Selected Contributions from FDL 2014
rédacteurs en chef	Frank Oppenheimer, Julio Luis Medina Pasaje
Editeur	Springer Verlag
Pages	3-22
Nombre de pages	20
ISBN (imprimé)	9783319244556
Les DOIs	https://doi.org/10.1007/978-3-319-24457-0_1
état	Publié - 1 janv. 2016
Modification externe	Oui
Evénement	16th Conference on Languages, Design Methods, and Tools for Electronic System Design, FDL 2014 - Munich, Allemagne Durée: 14 oct. 2014 → 16 oct. 2014

Série de publications

Nom	Lecture Notes in Electrical Engineering
Volume	361
ISSN (imprimé)	1876-1100
ISSN (Electronique)	1876-1119

Une conférence

Une conférence	16th Conference on Languages, Design Methods, and Tools for Electronic System Design, FDL 2014
Pays/Territoire	Allemagne
La ville	Munich
période	14/10/14 → 16/10/14

Accès au document

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

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

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

@inproceedings{d42f127fb19641fc9a6b8f10d091a0ca,

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

month = jan,

day = "1",

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. Dans 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, p. 3-22, 16th Conference on Languages, Design Methods, and Tools for Electronic System Design, FDL 2014, Munich, Allemagne, 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).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

TY - GEN

T1 - Automatic refinement checking for formal system models

AU - Seiter, Julia

AU - Wille, Robert

AU - Kühne, Ulrich

AU - Drechsler, Rolf

PY - 2016/1/1

Y1 - 2016/1/1

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 - https://www.scopus.com/pages/publications/84952774724

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

Résumé

Série de publications

Une conférence

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation