Define, verify, refine : correct composition and transformation of concurrent system semantics

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

8 Citations (Scopus)

Abstract

We present a technique to verify user-defined model transformations, in order to step-wise develop formal models of concurrent systems. The main benefit is that the changes applied to a model can be verified in isolation. In particular, the preservation of safety and liveness properties of such a modification can be determined independent of the input model. This is particularly useful for model-driven development approaches, where systems are designed and created by first developing an abstract model, and iteratively modifying this model until it is concrete enough to automatically generate source code from it. Properties that already hold on the initial model and should remain valid throughout the development in later models can be maintained with our tool Refiner, by which the effort of verifying those properties over and over again can be avoided. This paper generalises our earlier results in various ways, removing several restrictions, improving the focus of the verification method on transformations, and introducing the possibility to add completely new components at any time during the development.
Original languageEnglish
Title of host publicationProceedings of the 10th International Symposium on Formal Aspects of Component Software, FACS 2013, October 27-29, 2013, Nanchang, China, Revised Selected Papers
EditorsJ.L. Fiadeiro, Z. Liu, J. Xue
Place of PublicationBerlin
PublisherSpringer
Pages348-368
ISBN (Print)978-3-319-07601-0
DOIs
Publication statusPublished - 2013
Event10th International Symposium on Formal Aspects of Component Software (FACS 2013), October 27-29, 2013, Nanchang, China - Nanchang, China
Duration: 27 Oct 201329 Oct 2013

Publication series

NameLecture Notes in Computer Science
Volume8348
ISSN (Print)0302-9743

Conference

Conference10th International Symposium on Formal Aspects of Component Software (FACS 2013), October 27-29, 2013, Nanchang, China
Abbreviated titleFACS 2013
Country/TerritoryChina
CityNanchang
Period27/10/1329/10/13

Fingerprint

Dive into the research topics of 'Define, verify, refine : correct composition and transformation of concurrent system semantics'. Together they form a unique fingerprint.

Cite this