No Cover Image

Conference contribution 163 views 16 downloads

Formal Verification for Feature-Based Composition of Workflows / Stephan Adelsberger; Bashar Igried; Markus Moser; Vadim Savenkov; Anton Setzer

Pages: 173 - 181

Swansea University Author: Setzer, Anton

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!
first_indexed 2018-07-11T04:41:39Z
last_indexed 2018-12-27T13:51:40Z
id cronfa40970
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2018-12-27T12:18:16Z</datestamp><bib-version>v2</bib-version><id>40970</id><entry>2018-07-10</entry><title>Formal Verification for Feature-Based Composition of Workflows</title><alternativeTitle></alternativeTitle><author>Anton Setzer</author><firstname>Anton</firstname><surname>Setzer</surname><active>true</active><ORCID>0000-0001-5322-6060</ORCID><ethesisStudent>false</ethesisStudent><sid>5f7695285397f46d121207120247c2ae</sid><email>61db1ab5eaeff34062db71cc1973df39</email><emailaddr>QBY4tVYqSovxQSx/NwDRpMjwe531u+mO/3IG3xe5jMg=</emailaddr><date>2018-07-10</date><deptcode>SCS</deptcode><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.</abstract><type>Conference contribution</type><journal></journal><volume/><journalNumber/><paginationStart>173</paginationStart><paginationEnd>181</paginationEnd><publisher>SERENE 2018:10th International Workshop on Software Engineering for Resilient Systems</publisher><placeOfPublication>Iasi (Romania)</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords>feature-oriented software development, product-Based Workflows, Agda, theorem proving, dependable software, family-level formal verification, verification of workflows</keywords><publishedDay>12</publishedDay><publishedMonth>11</publishedMonth><publishedYear>2018</publishedYear><publishedDate>2018-11-12</publishedDate><doi>10.1109/EDCC.2018.00039</doi><url>http://www.cs.swan.ac.uk/~csetzer/articles/SERENE/SERENE18/SERENE18AdelsbergerIgriedMoserSavenkoSetzer.pdf</url><notes></notes><college>College of Science</college><department>Computer Science</department><CollegeCode>CSCI</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution/><researchGroup>Theoretical Computer Science</researchGroup><supervisor/><sponsorsfunders/><grantnumber/><degreelevel/><degreename>None</degreename><lastEdited>2018-12-27T12:18:16Z</lastEdited><Created>2018-07-10T23:38:28Z</Created><path><level id="1">College of Science</level><level id="2">Computer Science</level></path><authors><author><firstname>Stephan</firstname><surname>Adelsberger</surname><orcid/><order>1</order></author><author><firstname>Bashar</firstname><surname>Igried</surname><orcid/><order>2</order></author><author><firstname>Markus</firstname><surname>Moser</surname><orcid/><order>3</order></author><author><firstname>Vadim</firstname><surname>Savenkov</surname><orcid/><order>4</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid/><order>5</order></author></authors><documents><document><filename>0040970-10072018234640.pdf</filename><originalFilename>SERENE_2018_paper_8.pdf</originalFilename><uploaded>2018-07-10T23:46:40Z</uploaded><type>Output</type><contentLength>603042</contentLength><contentType>application/pdf</contentType><version>P</version><cronfaStatus>true</cronfaStatus><action>Published to Cronfa</action><actionDate>10/07/2018</actionDate><embargoDate>2019-01-10T00:00:00</embargoDate><documentNotes/><copyrightCorrect>false</copyrightCorrect><language>eng</language></document><document><filename>Under embargo</filename><originalFilename>Under embargo</originalFilename><uploaded>2018-07-26T02:07:37Z</uploaded><type>Output</type><contentLength>479940</contentLength><contentType>application/pdf</contentType><version>AM</version><cronfaStatus>true</cronfaStatus><action>Updated Embargo</action><actionDate>27/12/2018</actionDate><embargoDate>2019-11-12T00:00:00</embargoDate><documentNotes/><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents></rfc1807>
spelling 2018-12-27T12:18:16Z v2 40970 2018-07-10 Formal Verification for Feature-Based Composition of Workflows Anton Setzer Anton Setzer true 0000-0001-5322-6060 false 5f7695285397f46d121207120247c2ae 61db1ab5eaeff34062db71cc1973df39 QBY4tVYqSovxQSx/NwDRpMjwe531u+mO/3IG3xe5jMg= 2018-07-10 SCS 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. Conference contribution 173 181 SERENE 2018:10th International Workshop on Software Engineering for Resilient Systems Iasi (Romania) feature-oriented software development, product-Based Workflows, Agda, theorem proving, dependable software, family-level formal verification, verification of workflows 12 11 2018 2018-11-12 10.1109/EDCC.2018.00039 http://www.cs.swan.ac.uk/~csetzer/articles/SERENE/SERENE18/SERENE18AdelsbergerIgriedMoserSavenkoSetzer.pdf College of Science Computer Science CSCI SCS Theoretical Computer Science None 2018-12-27T12:18:16Z 2018-07-10T23:38:28Z College of Science Computer Science Stephan Adelsberger 1 Bashar Igried 2 Markus Moser 3 Vadim Savenkov 4 Anton Setzer 5 0040970-10072018234640.pdf SERENE_2018_paper_8.pdf 2018-07-10T23:46:40Z Output 603042 application/pdf P true Published to Cronfa 10/07/2018 2019-01-10T00:00:00 false eng Under embargo Under embargo 2018-07-26T02:07:37Z Output 479940 application/pdf AM true Updated Embargo 27/12/2018 2019-11-12T00:00:00 true eng
title Formal Verification for Feature-Based Composition of Workflows
spellingShingle Formal Verification for Feature-Based Composition of Workflows
Setzer, Anton
title_short Formal Verification for Feature-Based Composition of Workflows
title_full Formal Verification for Feature-Based Composition of Workflows
title_fullStr Formal Verification for Feature-Based Composition of Workflows
title_full_unstemmed Formal Verification for Feature-Based Composition of Workflows
title_sort Formal Verification for Feature-Based Composition of Workflows
author_id_str_mv 5f7695285397f46d121207120247c2ae
author_id_fullname_str_mv 5f7695285397f46d121207120247c2ae_***_Setzer, Anton
author Setzer, Anton
author2 Stephan Adelsberger
Bashar Igried
Markus Moser
Vadim Savenkov
Anton Setzer
format Conference contribution
container_start_page 173
publishDate 2018
institution Swansea University
doi_str_mv 10.1109/EDCC.2018.00039
publisher SERENE 2018:10th International Workshop on Software Engineering for Resilient Systems
college_str College of Science
hierarchytype
hierarchy_top_id collegeofscience
hierarchy_top_title College of Science
hierarchy_parent_id collegeofscience
hierarchy_parent_title College of Science
department_str Computer Science{{{_:::_}}}College of Science{{{_:::_}}}Computer Science
url http://www.cs.swan.ac.uk/~csetzer/articles/SERENE/SERENE18/SERENE18AdelsbergerIgriedMoserSavenkoSetzer.pdf
document_store_str 1
active_str 1
researchgroup_str Theoretical Computer Science
description 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.
published_date 2018-11-12T22:05:00Z
_version_ 1642693184801734656
score 10.837401