Adelsberger, Stephan, Igried, Bashar, Moser, Markus, Savenkov, Vadim, Setzer, Anton. 2018. Formal Verification for Feature-Based Composition of Workflows. In 14th European Dependable Computing Conference, EDCC 2018, Iasi, Romania, September 10-14, 2018, Hrsg. Emanuel Onica, Pascal Felber, Paolo Lollini, 173-181. Iasi: IEEE.
BibTeX
Abstract
We present FeatureAgda, a framework for specifying and proving properties of feature-based composition of workflows implemented in the Feature-Oriented Software Production Lines paradigm. The resulting workflows allow for adaptation at runtime by changing the set of enabled features. Our framework is based on Agda, which is both a theorem prover and a programming language. It relies on dependent types to support the modular definition of features. While promoting the separation of concerns, we obtain a single artefact written entirely in Agda, allowing family-level formal verification. As a practical application of our approach, we demonstrate a case study from the healthcare domain implementing a complex medication prescription workflow. Our setting allows the workflow to be changed to accommodate the needs of a particular doctor or clinic while having trustworthiness through formal verification.
Tags
Press 'enter' for creating the tagPublication's profile
Status of publication | Published |
---|---|
Affiliation | WU |
Type of publication | Contribution to conference proceedings |
Language | English |
Title | Formal Verification for Feature-Based Composition of Workflows |
Title of whole publication | 14th European Dependable Computing Conference, EDCC 2018, Iasi, Romania, September 10-14, 2018 |
Editor | Emanuel Onica, Pascal Felber, Paolo Lollini |
Page from | 173 |
Page to | 181 |
Location | Iasi |
Publisher | IEEE |
Year | 2018 |
ISBN | 978-1-5386-8060-5 |
URL | https://doi.org/10.1109/EDCC.2018.00039 |
Open Access | N |
Associations
- People
- Adelsberger, Stephan (Details)
- Savenkov, Vadim (Former researcher)
- External
- Igried, Bashar (Swansea University, United Kingdom)
- Moser, Markus (Vienna University of Economics and Business (WU), Austria)
- Setzer, Anton (University of Swansea, United Kingdom)
- Organization
- Institute for Data, Process and Knowledge Management (AE Polleres) (Details)
- Research areas (Ă–STAT Classification 'Statistik Austria')
- 1105 Computer software (Details)
- 3912 Computer-aided diagnosis and therapy (Details)