Formal Verification for Feature-based Composition of Workflows

  • Adelsberger, S. (Contributor)
  • Bashar Igried (Contributor)
  • Markus Moser (Contributor)
  • Vadim Savenkov (Contributor)
  • Anton Setzer (Contributor)

Activity: Talk or presentationScience to science


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.
Period10 Sept 201814 Sept 2018
Event title10th International Workshop on Software Engineering for Resilient Systems
Event typeUnknown
Degree of RecognitionInternational

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

  • 102015 Information systems
  • 102022 Software development
  • 102