The Community for Technology Leaders
2018 14th European Dependable Computing Conference (EDCC) (2018)
Ia?i, Romania
Sep 10, 2018 to Sep 14, 2018
ISBN: 978-1-5386-8060-5
pp: 173-181
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.
INDEX TERMS
formal verification, object-oriented programming, software product lines, theorem proving
CITATION

S. Adelsberger, B. Igried, M. Moser, V. Savenkov and A. Setzer, "Formal Verification for Feature-Based Composition of Workflows," 2018 14th European Dependable Computing Conference (EDCC), Ia?i, Romania, 2018, pp. 173-181.
doi:10.1109/EDCC.2018.00039
239 ms
(Ver 3.3 (11022016))