Weaving true-concurrent aspects using constraint solvers

Juliana K F Bowles, Behzad Bordbar, Mohammed Alwanain

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

7 Citations (Scopus)
219 Downloads (Pure)

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.
Original languageEnglish
Title of host publication16th International Conference on Application of Concurrency to System Design 2016
PublisherIEEE Xplore
Number of pages10
ISBN (Electronic)978-1-5090-2589-3
ISBN (Print)978-1-5090-0763-9
DOIs
Publication statusPublished - 6 Feb 2017
Event16th International Conference on Application of Concurrency to System Design (ACSD 2016) - Torun, Poland
Duration: 19 Jun 201624 Jun 2016

Publication series

NameInternational Conference on Application of Concurrency to System Design. Proceedings
ISSN (Print)1550-4808

Conference

Conference16th International Conference on Application of Concurrency to System Design (ACSD 2016)
Country/TerritoryPoland
CityTorun
Period19/06/1624/06/16

Fingerprint

Dive into the research topics of 'Weaving true-concurrent aspects using constraint solvers'. Together they form a unique fingerprint.

Cite this