Formal Verification for Feature-Based Composition of Workflows

Stephan Adelsberger, Bashar Igried, Markus Moser, Vadim Savenkov, Anton Setzer

Publication: Chapter in book/Conference proceedingContribution to conference proceedings

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.
Original languageEnglish
Title of host publication2018 14th European Dependable Computing Conference, EDCC 2018
EditorsJuan E. Guerrero
Place of PublicationIasi
PublisherIEEE
Pages173 - 181
Volume14
ISBN (Print)9781538680605
DOIs
Publication statusPublished - 2018

Austrian Classification of Fields of Science and Technology (ÖFOS)

  • 102022 Software development
  • 305901 Computer-aided diagnosis and therapy

Cite this