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


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
Pages173 - 181
ISBN (Print)9781538680605
Publication statusPublished - 2018

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

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

Cite this