Skip to content

Research at St Andrews

Correct composition of dephased behavioural models

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

DOI

Open Access permissions

Open

Abstract

Scenarios of execution are commonly used to specify partial behaviour and interactions between different objects and components in a system. To avoid overall inconsistency in specifications, various automated methods have emerged in the literature to compose (behavioural) models. In recent work, we have shown how the theorem prover Isabelle can be combined with the constraint solver Z3 to efficiently detect inconsistencies in two or more behavioural models and, in their absence, generate the composition. Here, we extend our approach further and show how to generate the correct composition (as a set of valid traces) of dephased models. This work has been inspired by a problem from a medical domain where different care pathways (for chronic conditions) may be applied to the same patient with different starting points.
Close

Details

Original languageEnglish
Title of host publicationFormal Aspects of Component Software
Subtitle of host publication14th International Conference, FACS 2017, Braga, Portugal, October 10-13, 2017, Proceedings
EditorsJosé Proença, Markus Lumpe
PublisherSpringer
Pages233-250
Number of pages18
ISBN (Electronic)9783319680347
ISBN (Print)9783319680330
DOIs
StatePublished - 2017
Event14th International Conference on Formal Aspects of Component Software - Braga, Portugal

Publication series

NameLecture Notes in Computer Science (Programming and Software Engineering)
PublisherSpringer
Volume10487
ISSN (Print)0302-9743

Conference

Conference14th International Conference on Formal Aspects of Component Software
Abbreviated titleFACS
CountryPortugal
CityBraga
Period10/10/1713/10/17
Internet address

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

View graph of relations

Related by author

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

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

    Bowles, J. K. F. & Caminati, M. B. 2017 Formal Methods and Software Engineering: 19th International Conference on Formal Engineering Methods, ICFEM 2017, Xi'an, China, November 13-17, 2017, Proceedings. Duan, Z. & Ong, L. (eds.). Springer, p. 209-225 16 p. (Lecture Notes in Computer Science (Programming and Software Engineering); vol. 10610)

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

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

  4. Mind the gap: addressing behavioural inconsistencies with formal methods

    Bowles, J. K. F. & Caminati, M. B. 6 Dec 2016 2016 23rd Asia-Pacific Software Engineering Conference (APSEC). Potanin, A., Murphy, G. C., Reeves, S. & Dietrich, J. (eds.). IEEE Computer Society, p. 313-320 8 p. 7890603

    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: 250701579