Skip to content

Research at St Andrews

Mind the gap: addressing behavioural inconsistencies with formal methods

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

DOI

Open Access permissions

Open

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

Details

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
StatePublished - 6 Dec 2016
Event23rd Asia-Pacific Software Engineering Conference - Hamilton, New Zealand

Conference

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

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Correct composition of dephased behavioural models

    Bowles, J. K. F. & Caminati, M. B. 18 Jul 2017 Formal Aspects of Component Software: 14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings. Springer, 18 p. (Lecture Notes in Computer Science (Programming and Software Engineering); vol. 10487)

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

  2. A flexible approach for finding optimal paths with minimal conflicts

    Bowles, J. K. F. & Caminati, M. B. 2 Jul 2017 19th International Conference on Formal Engineering Methods (ICFEM 2017). Springer, 16 p. (Lecture Notes in Computer Science)

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

  3. An integrated framework for verifying multiple care pathways

    Bowles, J. K. F., Caminati, M. B. & Cha, S. 23 May 2017 Eleventh International Symposium on Theoretical Aspects of Software Engineering. IEEE Computer Society, 8 p.

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

  4. A verified algorithm enumerating event structures

    Bowles, J. K. F. & Caminati, M. B. 2017 Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. Geuvers, H., England, M., Hasan, O., Rabe, F. & Teschke, O. (eds.). Cham: Springer, p. 239-254 (Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence); vol. 10383)

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

  5. Aplicação de técnicas quantitativas de modelagem na busca da eficiência de processos hospitalares

    Webber, T., Caminati, M. B., Mueller, M., Redeker, G., Bowles, J. K. F., Czekster, R. & Quickert, S. 23 Sep 2016

    Research output: Contribution to conferencePoster

ID: 246034971