No Cover Image

Conference Paper/Proceeding/Abstract 1235 views 324 downloads

Formal Verification for Feature-Based Composition of Workflows

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

Pages: 173 - 181

Swansea University Author: Anton Setzer Orcid Logo

DOI (Published version): 10.1109/EDCC.2018.00039

Abstract

We developed a framework to specify and prove properties of feature-based composition of workflows. Specifically, we use techniques from feature-oriented software development and apply them to implement workflows that vary depending on which of several features are enabled. Our framework allows the...

Full description

Published: Iasi (Romania) SERENE 2018:10th International Workshop on Software Engineering for Resilient Systems 2018
Online Access: http://www.cs.swan.ac.uk/~csetzer/articles/SERENE/SERENE18/SERENE18AdelsbergerIgriedMoserSavenkoSetzer.pdf
URI: https://cronfa.swan.ac.uk/Record/cronfa40970
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: We developed a framework to specify and prove properties of feature-based composition of workflows. Specifically, we use techniques from feature-oriented software development and apply them to implement workflows that vary depending on which of several features are enabled. Our framework allows the modular definition of features and promotes the separation of concerns in the workflow definitions. In addition, we obtain a single artefact that represents the entire software product line through the use of the expressiveness of dependent types, allowing the application of family-level formal verification.Our framework is based on Agda which is both a theorem prover and a programming language. We apply our framework to a case study from the healthcare domain which implements feature-based composition of workflows for medication prescriptions. Our setting allows the workflow to be changed according to patients' specific cases and doctors' needs while having trustworthiness through formal verification.
Keywords: feature-oriented software development, product-Based Workflows, Agda, theorem proving, dependable software, family-level formal verification, verification of workflows
College: Faculty of Science and Engineering
Start Page: 173
End Page: 181

Similar Items