E-Thesis 561 views 115 downloads
Developing proof technology for CSP-CASL. / Liam O'Reilly
Swansea University Author: Liam O'Reilly
-
PDF | E-Thesis
Download (4.6MB)
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...
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.0299 |