No Cover Image

Book chapter 1422 views

Verification of Scheme Plans Using CSP || B

Hoang Nguyen Orcid Logo, Philip James, Faron Moller Orcid Logo, Hoang Nga Nguyen, Markus Roggenbach, Steve Schneider, Helen Treharne, Matthew Trumble, David Williams

Software Engineering and Formal Methods, Volume: 8368

Swansea University Authors: Hoang Nguyen Orcid Logo, Faron Moller Orcid Logo

Full text not available from this repository: check for access using links below.

DOI (Published version): 10.1007/978-3-319-05032-4_15

Abstract

This paper presents a tool-supported approach to graphically editing scheme plans and their safety verification. The graphical tool is based on a domain-specific language which is used as a basis for a transformation to a CSP||B formal model of a scheme plan. The models produce use a variety of abst...

Full description

Published in: Software Engineering and Formal Methods
Published: 2014
URI: https://cronfa.swan.ac.uk/Record/cronfa20838
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2015-07-02T02:05:05Z
last_indexed 2018-02-09T04:57:48Z
id cronfa20838
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2017-06-09T16:47:49.7819571</datestamp><bib-version>v2</bib-version><id>20838</id><entry>2015-04-22</entry><title>Verification of Scheme Plans Using CSP || B</title><swanseaauthors><author><sid>cb24d5c5080534dc5b5e3390f24dd422</sid><ORCID>0000-0003-0260-1697</ORCID><firstname>Hoang</firstname><surname>Nguyen</surname><name>Hoang Nguyen</name><active>true</active><ethesisStudent>false</ethesisStudent></author><author><sid>bf25e0b52fe7c11c473cc48d306073f7</sid><ORCID>0000-0001-9535-8053</ORCID><firstname>Faron</firstname><surname>Moller</surname><name>Faron Moller</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2015-04-22</date><deptcode>SCS</deptcode><abstract>This paper presents a tool-supported approach to graphically editing scheme plans and their safety verification. The graphical tool is based on a domain-specific language which is used as a basis for a transformation to a CSP||B formal model of a scheme plan. The models produce use a variety of abstraction techniques that make the analysis of large scale plans feasible.</abstract><type>Book chapter</type><journal>Software Engineering and Formal Methods</journal><volume>8368</volume><paginationEnd>204</paginationEnd><publisher/><keywords/><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2014</publishedYear><publishedDate>2014-12-31</publishedDate><doi>10.1007/978-3-319-05032-4_15</doi><url/><notes>Originality:The paper makes the bold step of bringing mathematical theory down to the level of engineering practice; something rare, explaining why the type of formal methods presented are not readily adapted in practice. This is done through the use of a bespoke graphical tool based on a domain specific language inspired by engineering practice.Significance:The methodology outlined in this paper forms the basis of the technology being adapted by Siemens, which is the foundation of the REF Impact Case Study.Rigour:The methodology is, of course, founded on the most rigorous of mathematical theory development.</notes><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>SCS</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2017-06-09T16:47:49.7819571</lastEdited><Created>2015-04-22T09:48:04.6274874</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>Hoang</firstname><surname>Nguyen</surname><orcid>0000-0003-0260-1697</orcid><order>1</order></author><author><firstname>Philip</firstname><surname>James</surname><order>2</order></author><author><firstname>Faron</firstname><surname>Moller</surname><orcid>0000-0001-9535-8053</orcid><order>3</order></author><author><firstname>Hoang Nga</firstname><surname>Nguyen</surname><order>4</order></author><author><firstname>Markus</firstname><surname>Roggenbach</surname><order>5</order></author><author><firstname>Steve</firstname><surname>Schneider</surname><order>6</order></author><author><firstname>Helen</firstname><surname>Treharne</surname><order>7</order></author><author><firstname>Matthew</firstname><surname>Trumble</surname><order>8</order></author><author><firstname>David</firstname><surname>Williams</surname><order>9</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2017-06-09T16:47:49.7819571 v2 20838 2015-04-22 Verification of Scheme Plans Using CSP || B cb24d5c5080534dc5b5e3390f24dd422 0000-0003-0260-1697 Hoang Nguyen Hoang Nguyen true false bf25e0b52fe7c11c473cc48d306073f7 0000-0001-9535-8053 Faron Moller Faron Moller true false 2015-04-22 SCS This paper presents a tool-supported approach to graphically editing scheme plans and their safety verification. The graphical tool is based on a domain-specific language which is used as a basis for a transformation to a CSP||B formal model of a scheme plan. The models produce use a variety of abstraction techniques that make the analysis of large scale plans feasible. Book chapter Software Engineering and Formal Methods 8368 204 31 12 2014 2014-12-31 10.1007/978-3-319-05032-4_15 Originality:The paper makes the bold step of bringing mathematical theory down to the level of engineering practice; something rare, explaining why the type of formal methods presented are not readily adapted in practice. This is done through the use of a bespoke graphical tool based on a domain specific language inspired by engineering practice.Significance:The methodology outlined in this paper forms the basis of the technology being adapted by Siemens, which is the foundation of the REF Impact Case Study.Rigour:The methodology is, of course, founded on the most rigorous of mathematical theory development. COLLEGE NANME Computer Science COLLEGE CODE SCS Swansea University 2017-06-09T16:47:49.7819571 2015-04-22T09:48:04.6274874 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Hoang Nguyen 0000-0003-0260-1697 1 Philip James 2 Faron Moller 0000-0001-9535-8053 3 Hoang Nga Nguyen 4 Markus Roggenbach 5 Steve Schneider 6 Helen Treharne 7 Matthew Trumble 8 David Williams 9
title Verification of Scheme Plans Using CSP || B
spellingShingle Verification of Scheme Plans Using CSP || B
Hoang Nguyen
Faron Moller
title_short Verification of Scheme Plans Using CSP || B
title_full Verification of Scheme Plans Using CSP || B
title_fullStr Verification of Scheme Plans Using CSP || B
title_full_unstemmed Verification of Scheme Plans Using CSP || B
title_sort Verification of Scheme Plans Using CSP || B
author_id_str_mv cb24d5c5080534dc5b5e3390f24dd422
bf25e0b52fe7c11c473cc48d306073f7
author_id_fullname_str_mv cb24d5c5080534dc5b5e3390f24dd422_***_Hoang Nguyen
bf25e0b52fe7c11c473cc48d306073f7_***_Faron Moller
author Hoang Nguyen
Faron Moller
author2 Hoang Nguyen
Philip James
Faron Moller
Hoang Nga Nguyen
Markus Roggenbach
Steve Schneider
Helen Treharne
Matthew Trumble
David Williams
format Book chapter
container_title Software Engineering and Formal Methods
container_volume 8368
publishDate 2014
institution Swansea University
doi_str_mv 10.1007/978-3-319-05032-4_15
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
document_store_str 0
active_str 0
description This paper presents a tool-supported approach to graphically editing scheme plans and their safety verification. The graphical tool is based on a domain-specific language which is used as a basis for a transformation to a CSP||B formal model of a scheme plan. The models produce use a variety of abstraction techniques that make the analysis of large scale plans feasible.
published_date 2014-12-31T03:24:40Z
_version_ 1763750844221620224
score 11.016235