Skip to content

Research at St Andrews

Weaving true-concurrent aspects using constraint solvers

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

DOI

Open Access permissions

Open

Author(s)

Juliana Kuster Filipe Bowles, Behzad Bordbar, Mohammed Alwanain

School/Research organisations

Abstract

Large system models usually consist of several simpler models that can be understood more easily. Making changes to the behaviour of a component will likely affect several models and could introduce accidental errors. Aspects
address this by modelling new functionality required in several places as an
advice, which can be integrated with the original base models by specifying a
pointcut. Before checking that the overall outcome is correct, we need to weave the cross-cutting advice into the base models, and obtain new augmented
models. Although considerable research has been done to weave models, many such approaches are not fully automated. This paper looks at aspect weaving of scenario-based models, where aspects are given a true-concurrent semantics based on event structures. Our contribution is a novel formal automated
technique for weaving aspects using the Z3-SMT solver. We compare the performance of Alloy and Z3 to justify our choice.
Close

Details

Original languageEnglish
Title of host publication2016 16th International Conference on Application of Concurrency to System Design (ACSD)
PublisherIEEE Computer Society
Pages35-44
Number of pages10
ISBN (Print)9781509025893
DOIs
StatePublished - 3 Feb 2017
EventPN 2016 // ACSD 2016 - Toruń, Poland

Conference

ConferencePN 2016 // ACSD 2016
Abbreviated titleACSD
CountryPoland
CityToruń
Period19/06/1624/06/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. Estimating capacity and resource allocation in healthcare settings using business process modelling and simulation

    Redeker, G., Webber, T., Czekster, R., Quickert, S. & Bowles, J. K. F. 2 Jul 2017 Anais XXXVII Congresso da Sociedade Brasileira de Computação. Sociedade Brasileira de Computação (SBC), p. 1979-1982

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

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

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

  5. Formal verification of CNL health recommendations

    Rahman, F. & Bowles, J. K. F. 2017 Integrated Formal Methods: 13th International Conference, IFM 2017, Turin, Italy, September 20-22, 2017, Proceedings. Polikarpova, N. & Schneider, S. (eds.). Cham: Springer, p. 357-371 15 p. (Lecture Notes in Computer Science (Programming and Software Engineering); vol. 10510)

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

ID: 241963085