No Cover Image

E-Thesis 454 views 91 downloads

Developing proof technology for CSP-CASL. / Liam O'Reilly

Swansea University Author: Liam O'Reilly

Abstract

Distributed applications such as flight booking systems, web services, and electronic payment systems require parallel processing of data. Such systems exhibit concurrent aspects (e.g., deadlock freedom) as well as data aspects (e.g., functional correctness). Often, these two aspects depend on each...

Full description

Published: 2008
Institution: Swansea University
Degree level: Master of Philosophy
Degree name: M.Phil
URI: https://cronfa.swan.ac.uk/Record/cronfa42789
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2018-08-02T18:55:33Z
last_indexed 2019-10-21T16:48:28Z
id cronfa42789
recordtype RisThesis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2018-08-16T14:39:02.9105634</datestamp><bib-version>v2</bib-version><id>42789</id><entry>2018-08-02</entry><title>Developing proof technology for CSP-CASL.</title><swanseaauthors><author><sid>df0cea457a934d2bddf04638a83fc665</sid><ORCID>NULL</ORCID><firstname>Liam</firstname><surname>O'Reilly</surname><name>Liam O'Reilly</name><active>true</active><ethesisStudent>true</ethesisStudent></author></swanseaauthors><date>2018-08-02</date><abstract>Distributed applications such as flight booking systems, web services, and electronic payment systems require parallel processing of data. Such systems exhibit concurrent aspects (e.g., deadlock freedom) as well as data aspects (e.g., functional correctness). Often, these two aspects depend on each other. The language CSP-CASL is tailored to the specification and verification of such distributed systems and allows one to model data as well as processes within a single framework. In this thesis we explore methods and techniques tailored to theorem proving for CSP-CASL. This leads to the development of an architecture for CSP-CASL-Prover which re-uses the tools HETS and CSP-Prover. We also design - up to the algorithmic level - procedures for transforming a CSP- CASL specification into Isabelle/HOL code whilst preserving the semantics. By using this translation, it is possible to perform theorem proving on CSP-CASL specifications using Isabelle/HOL. As proof of concept we validate our tool CSP-CASL-Prover on a case study of industrial strength. Our experiment shows that CSP-CASL-Prover scales up to large systems. When using CSP-CASL-Prover reasoning about CSP-CASL specifications becomes as easy as reasoning about data and processes separately.</abstract><type>E-Thesis</type><journal/><journalNumber></journalNumber><paginationStart/><paginationEnd/><publisher/><placeOfPublication/><isbnPrint/><issnPrint/><issnElectronic/><keywords>Computer science.</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2008</publishedYear><publishedDate>2008-12-31</publishedDate><doi/><url/><notes/><college>COLLEGE NANME</college><department>Computer Science</department><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><degreelevel>Master of Philosophy</degreelevel><degreename>M.Phil</degreename><apcterm/><lastEdited>2018-08-16T14:39:02.9105634</lastEdited><Created>2018-08-02T16:24:30.4921985</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>Liam</firstname><surname>O'Reilly</surname><orcid>NULL</orcid><order>1</order></author></authors><documents><document><filename>0042789-02082018162522.pdf</filename><originalFilename>10807565.pdf</originalFilename><uploaded>2018-08-02T16:25:22.0370000</uploaded><type>Output</type><contentLength>4745246</contentLength><contentType>application/pdf</contentType><version>E-Thesis</version><cronfaStatus>true</cronfaStatus><embargoDate>2018-08-02T16:25:22.0370000</embargoDate><copyrightCorrect>false</copyrightCorrect></document></documents><OutputDurs/></rfc1807>
spelling 2018-08-16T14:39:02.9105634 v2 42789 2018-08-02 Developing proof technology for CSP-CASL. df0cea457a934d2bddf04638a83fc665 NULL Liam O'Reilly Liam O'Reilly true true 2018-08-02 Distributed applications such as flight booking systems, web services, and electronic payment systems require parallel processing of data. Such systems exhibit concurrent aspects (e.g., deadlock freedom) as well as data aspects (e.g., functional correctness). Often, these two aspects depend on each other. The language CSP-CASL is tailored to the specification and verification of such distributed systems and allows one to model data as well as processes within a single framework. In this thesis we explore methods and techniques tailored to theorem proving for CSP-CASL. This leads to the development of an architecture for CSP-CASL-Prover which re-uses the tools HETS and CSP-Prover. We also design - up to the algorithmic level - procedures for transforming a CSP- CASL specification into Isabelle/HOL code whilst preserving the semantics. By using this translation, it is possible to perform theorem proving on CSP-CASL specifications using Isabelle/HOL. As proof of concept we validate our tool CSP-CASL-Prover on a case study of industrial strength. Our experiment shows that CSP-CASL-Prover scales up to large systems. When using CSP-CASL-Prover reasoning about CSP-CASL specifications becomes as easy as reasoning about data and processes separately. E-Thesis Computer science. 31 12 2008 2008-12-31 COLLEGE NANME Computer Science COLLEGE CODE Swansea University Master of Philosophy M.Phil 2018-08-16T14:39:02.9105634 2018-08-02T16:24:30.4921985 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Liam O'Reilly NULL 1 0042789-02082018162522.pdf 10807565.pdf 2018-08-02T16:25:22.0370000 Output 4745246 application/pdf E-Thesis true 2018-08-02T16:25:22.0370000 false
title Developing proof technology for CSP-CASL.
spellingShingle Developing proof technology for CSP-CASL.
Liam O'Reilly
title_short Developing proof technology for CSP-CASL.
title_full Developing proof technology for CSP-CASL.
title_fullStr Developing proof technology for CSP-CASL.
title_full_unstemmed Developing proof technology for CSP-CASL.
title_sort Developing proof technology for CSP-CASL.
author_id_str_mv df0cea457a934d2bddf04638a83fc665
author_id_fullname_str_mv df0cea457a934d2bddf04638a83fc665_***_Liam O'Reilly
author Liam O'Reilly
author2 Liam O'Reilly
format E-Thesis
publishDate 2008
institution Swansea University
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 1
active_str 0
description Distributed applications such as flight booking systems, web services, and electronic payment systems require parallel processing of data. Such systems exhibit concurrent aspects (e.g., deadlock freedom) as well as data aspects (e.g., functional correctness). Often, these two aspects depend on each other. The language CSP-CASL is tailored to the specification and verification of such distributed systems and allows one to model data as well as processes within a single framework. In this thesis we explore methods and techniques tailored to theorem proving for CSP-CASL. This leads to the development of an architecture for CSP-CASL-Prover which re-uses the tools HETS and CSP-Prover. We also design - up to the algorithmic level - procedures for transforming a CSP- CASL specification into Isabelle/HOL code whilst preserving the semantics. By using this translation, it is possible to perform theorem proving on CSP-CASL specifications using Isabelle/HOL. As proof of concept we validate our tool CSP-CASL-Prover on a case study of industrial strength. Our experiment shows that CSP-CASL-Prover scales up to large systems. When using CSP-CASL-Prover reasoning about CSP-CASL specifications becomes as easy as reasoning about data and processes separately.
published_date 2008-12-31T03:53:39Z
_version_ 1763752667478228992
score 11.012678

Similar Items