On the Feasibility of a Unified Modelling and Programming Paradigm

Anne Elisabeth Haxthausen; Jan Peleska

doi:10.1007/978-3-319-47169-3_4

On the Feasibility of a Unified Modelling and Programming Paradigm

Anne Elisabeth Haxthausen
, Jan Peleska

Department of Applied Mathematics and Computer Science

University of Bremen

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

373 Downloads (Orbit)

Abstract

In this article, the feasibility of a unified modelling and programming paradigm is discussed from the perspective of large scale system development and verification in collaborative development environments. We motivate the necessity to utilise multiple formalisms for development and verification, in particular for complex cyber-physical systems or systems of systems. Though modelling, programming, and verification will certainly become more closely integrated in the future, we do not expect a single formalism to become universally applicable and accepted by the development and verification communities. The multi-formalism approach requires to translate verification artefacts (assertions, test cases, etc.) between different representations, in order to allow for the verification of emergent properties based on local verification results established with different methods and modelling techniques. It is illustrated by means of a case study from the railway domain, how this can be achieved, using concepts from the theory of institutions. This also enables the utilisation of verification tools in different formalisms, despite the fact that these tools are usually developed for one specific formal method.

Original language	English
Title of host publication	Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016) : Discussion, Dissemination, Applications - Part II
Publisher	Springer
Publication date	2016
Pages	32-49
ISBN (Print)	978-3-319-47168-6
ISBN (Electronic)	978-3-319-47169-3
DOIs	https://doi.org/10.1007/978-3-319-47169-3_4
Publication status	Published - 2016
Event	7^th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation - Corfu, Greece Duration: 10 Oct 2016 → 14 Oct 2016 Conference number: 7

Conference

Conference	7^th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation
Number	7
Country/Territory	Greece
City	Corfu
Period	10/10/2016 → 14/10/2016

Series	Lecture Notes in Computer Science
Volume	9953
ISSN	0302-9743

Access to Document

10.1007/978-3-319-47169-3_4

MainAccepted author manuscript, 567 KB

OpenUrl availability

Check availability in DTU Findit

Cite this

Haxthausen, Anne Elisabeth ; Peleska, Jan. / On the Feasibility of a Unified Modelling and Programming Paradigm. Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016): Discussion, Dissemination, Applications - Part II. Springer, 2016. pp. 32-49 (Lecture Notes in Computer Science, Vol. 9953).

@inproceedings{67cf239092f74c9b807057e774452863,

title = "On the Feasibility of a Unified Modelling and Programming Paradigm",

abstract = "In this article, the feasibility of a unified modelling and programming paradigm is discussed from the perspective of large scale system development and verification in collaborative development environments. We motivate the necessity to utilise multiple formalisms for development and verification, in particular for complex cyber-physical systems or systems of systems. Though modelling, programming, and verification will certainly become more closely integrated in the future, we do not expect a single formalism to become universally applicable and accepted by the development and verification communities. The multi-formalism approach requires to translate verification artefacts (assertions, test cases, etc.) between different representations, in order to allow for the verification of emergent properties based on local verification results established with different methods and modelling techniques. It is illustrated by means of a case study from the railway domain, how this can be achieved, using concepts from the theory of institutions. This also enables the utilisation of verification tools in different formalisms, despite the fact that these tools are usually developed for one specific formal method.",

author = "Haxthausen, \{Anne Elisabeth\} and Jan Peleska",

year = "2016",

doi = "10.1007/978-3-319-47169-3\_4",

language = "English",

isbn = "978-3-319-47168-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "32--49",

booktitle = "Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016)",

note = "7<sup>th</sup> International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 ; Conference date: 10-10-2016 Through 14-10-2016",

}

Haxthausen, AE & Peleska, J 2016, On the Feasibility of a Unified Modelling and Programming Paradigm. in Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016): Discussion, Dissemination, Applications - Part II. Springer, Lecture Notes in Computer Science, vol. 9953, pp. 32-49, 7^th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Corfu, Greece, 10/10/2016. https://doi.org/10.1007/978-3-319-47169-3_4

On the Feasibility of a Unified Modelling and Programming Paradigm. / Haxthausen, Anne Elisabeth; Peleska, Jan.
Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016): Discussion, Dissemination, Applications - Part II. Springer, 2016. p. 32-49 (Lecture Notes in Computer Science, Vol. 9953).

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

TY - GEN

T1 - On the Feasibility of a Unified Modelling and Programming Paradigm

AU - Haxthausen, Anne Elisabeth

AU - Peleska, Jan

N1 - Conference code: 7

PY - 2016

Y1 - 2016

N2 - In this article, the feasibility of a unified modelling and programming paradigm is discussed from the perspective of large scale system development and verification in collaborative development environments. We motivate the necessity to utilise multiple formalisms for development and verification, in particular for complex cyber-physical systems or systems of systems. Though modelling, programming, and verification will certainly become more closely integrated in the future, we do not expect a single formalism to become universally applicable and accepted by the development and verification communities. The multi-formalism approach requires to translate verification artefacts (assertions, test cases, etc.) between different representations, in order to allow for the verification of emergent properties based on local verification results established with different methods and modelling techniques. It is illustrated by means of a case study from the railway domain, how this can be achieved, using concepts from the theory of institutions. This also enables the utilisation of verification tools in different formalisms, despite the fact that these tools are usually developed for one specific formal method.

AB - In this article, the feasibility of a unified modelling and programming paradigm is discussed from the perspective of large scale system development and verification in collaborative development environments. We motivate the necessity to utilise multiple formalisms for development and verification, in particular for complex cyber-physical systems or systems of systems. Though modelling, programming, and verification will certainly become more closely integrated in the future, we do not expect a single formalism to become universally applicable and accepted by the development and verification communities. The multi-formalism approach requires to translate verification artefacts (assertions, test cases, etc.) between different representations, in order to allow for the verification of emergent properties based on local verification results established with different methods and modelling techniques. It is illustrated by means of a case study from the railway domain, how this can be achieved, using concepts from the theory of institutions. This also enables the utilisation of verification tools in different formalisms, despite the fact that these tools are usually developed for one specific formal method.

U2 - 10.1007/978-3-319-47169-3_4

DO - 10.1007/978-3-319-47169-3_4

M3 - Article in proceedings

SN - 978-3-319-47168-6

T3 - Lecture Notes in Computer Science

SP - 32

EP - 49

BT - Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016)

PB - Springer

T2 - 7<sup>th</sup> International Symposium on Leveraging Applications of Formal Methods, Verification and Validation

Y2 - 10 October 2016 through 14 October 2016

ER -

Haxthausen AE, Peleska J. On the Feasibility of a Unified Modelling and Programming Paradigm. In Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2016): Discussion, Dissemination, Applications - Part II. Springer. 2016. p. 32-49. (Lecture Notes in Computer Science, Vol. 9953). doi: 10.1007/978-3-319-47169-3_4

On the Feasibility of a Unified Modelling and Programming Paradigm

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this