No Cover Image

Conference Paper/Proceeding/Abstract 1230 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!
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:16.2966918</datestamp><bib-version>v2</bib-version><id>40970</id><entry>2018-07-10</entry><title>Formal Verification for Feature-Based Composition of Workflows</title><swanseaauthors><author><sid>5f7695285397f46d121207120247c2ae</sid><ORCID>0000-0001-5322-6060</ORCID><firstname>Anton</firstname><surname>Setzer</surname><name>Anton Setzer</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><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 Paper/Proceeding/Abstract</type><journal/><paginationStart>173</paginationStart><paginationEnd>181</paginationEnd><publisher>SERENE 2018:10th International Workshop on Software Engineering for Resilient Systems</publisher><placeOfPublication>Iasi (Romania)</placeOfPublication><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/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2018-12-27T12:18:16.2966918</lastEdited><Created>2018-07-10T23:38:28.5170246</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Stephan</firstname><surname>Adelsberger</surname><order>1</order></author><author><firstname>Bashar</firstname><surname>Igried</surname><order>2</order></author><author><firstname>Markus</firstname><surname>Moser</surname><order>3</order></author><author><firstname>Vadim</firstname><surname>Savenkov</surname><order>4</order></author><author><firstname>Anton</firstname><surname>Setzer</surname><orcid>0000-0001-5322-6060</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:40.6100000</uploaded><type>Output</type><contentLength>603042</contentLength><contentType>application/pdf</contentType><version>Proof</version><cronfaStatus>true</cronfaStatus><embargoDate>2019-01-10T00:00:00.0000000</embargoDate><copyrightCorrect>false</copyrightCorrect><language>eng</language></document><document><filename>0040970-26072018020737.pdf</filename><originalFilename>SERENE18AdelsbergerIgriedMoserSavenkovSetzerfinal.pdf</originalFilename><uploaded>2018-07-26T02:07:37.4030000</uploaded><type>Output</type><contentLength>479940</contentLength><contentType>application/pdf</contentType><version>Accepted Manuscript</version><cronfaStatus>true</cronfaStatus><embargoDate>2019-11-12T00:00:00.0000000</embargoDate><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2018-12-27T12:18:16.2966918 v2 40970 2018-07-10 Formal Verification for Feature-Based Composition of Workflows 5f7695285397f46d121207120247c2ae 0000-0001-5322-6060 Anton Setzer Anton Setzer true false 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 Paper/Proceeding/Abstract 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 NANME Computer Science COLLEGE CODE SCS Swansea University 2018-12-27T12:18:16.2966918 2018-07-10T23:38:28.5170246 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Stephan Adelsberger 1 Bashar Igried 2 Markus Moser 3 Vadim Savenkov 4 Anton Setzer 0000-0001-5322-6060 5 0040970-10072018234640.pdf SERENE_2018_paper_8.pdf 2018-07-10T23:46:40.6100000 Output 603042 application/pdf Proof true 2019-01-10T00:00:00.0000000 false eng 0040970-26072018020737.pdf SERENE18AdelsbergerIgriedMoserSavenkovSetzerfinal.pdf 2018-07-26T02:07:37.4030000 Output 479940 application/pdf Accepted Manuscript true 2019-11-12T00:00:00.0000000 true eng
title Formal Verification for Feature-Based Composition of Workflows
spellingShingle Formal Verification for Feature-Based Composition of Workflows
Anton Setzer
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_***_Anton Setzer
author Anton Setzer
author2 Stephan Adelsberger
Bashar Igried
Markus Moser
Vadim Savenkov
Anton Setzer
format Conference Paper/Proceeding/Abstract
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 Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://www.cs.swan.ac.uk/~csetzer/articles/SERENE/SERENE18/SERENE18AdelsbergerIgriedMoserSavenkoSetzer.pdf
document_store_str 1
active_str 0
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-12T03:52:12Z
_version_ 1763752576138870784
score 11.036706

Similar Items