Mind the gap: addressing behavioural inconsistencies with formal methods

Juliana Kuster Filipe Bowles, Marco Bright Caminati

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)
2 Downloads (Pure)

Abstract

In complex system design, it is important to construct several design models focusing on different aspects of a system to gain a better understanding of individual component structure and behaviour. Scenarios of execution are commonly used to specify partial behaviour and interactions between a group of system objects or components. However, partial specifications may hide inconsistencies or an otherwise unintentionally incomplete or underspecified behavioural model. This paper proposes a new powerful technique combining constraint solvers and theorem provers to complete partial specifications and determine overall model inconsistencies. We use a true-concurrent model, namely labelled event structures, which can be used as the underlying semantics of widely used work flow or scenario-based languages. We show how an interplay between the theorem prover Isabelle and constraint solver Z3 can be used for detecting and solving partial specifications and inconsistencies over event structures.
Original languageEnglish
Title of host publication2016 23rd Asia-Pacific Software Engineering Conference (APSEC)
EditorsAlex Potanin, Gail C. Murphy, Steve Reeves, Jens Dietrich
PublisherIEEE Computer Society
Pages313-320
Number of pages8
ISBN (Electronic)9781509055753
DOIs
Publication statusPublished - 6 Dec 2016
Event23rd Asia-Pacific Software Engineering Conference - University of Waikato, Hamilton, New Zealand
Duration: 6 Dec 20169 Dec 2016
Conference number: 23
http://www.apsec2016.org/index.html

Conference

Conference23rd Asia-Pacific Software Engineering Conference
Abbreviated titleAPSEC
Country/TerritoryNew Zealand
CityHamilton
Period6/12/169/12/16
Internet address

Fingerprint

Dive into the research topics of 'Mind the gap: addressing behavioural inconsistencies with formal methods'. Together they form a unique fingerprint.

Cite this