No Cover Image

E-Thesis 529 views 339 downloads

Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification / BASHAR ALKHAWALDEH

Swansea University Author: BASHAR ALKHAWALDEH

DOI (Published version): 10.23889/Suthesis.54270

Abstract

We introduce a library called CSP-Agda for representing processes in the dependently typed theorem prover and interactive programming language Agda. We will enhance processes by a monad structure. The monad struc-ture facilitates combining processes in a modular way, and allows to define recursion a...

Full description

Published: Swansea 2018
Institution: Swansea University
Degree level: Doctoral
Degree name: Ph.D
Supervisor: Setzer, Anton ; Berger, Ulrich
URI: https://cronfa.swan.ac.uk/Record/cronfa54270
first_indexed 2020-05-18T19:08:46Z
last_indexed 2020-05-19T13:10:25Z
id cronfa54270
recordtype RisThesis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2020-05-19T11:36:53.5964703</datestamp><bib-version>v2</bib-version><id>54270</id><entry>2020-05-18</entry><title>Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification</title><swanseaauthors><author><sid>997fec2a691e4337ef78f7b096636ca1</sid><firstname>BASHAR</firstname><surname>ALKHAWALDEH</surname><name>BASHAR ALKHAWALDEH</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2020-05-18</date><abstract>We introduce a library called CSP-Agda for representing processes in the dependently typed theorem prover and interactive programming language Agda. We will enhance processes by a monad structure. The monad struc-ture facilitates combining processes in a modular way, and allows to define recursion as a direct operation on processes. Processes are defined coinduc-tively as non-well-founded trees. The nodes of the tree are formed by a an atomic one step relation, which determines for a process the external, internal choices, and termination events it can choose, and whether the process has terminated. The data type of processes is inspired by Setzer and Hancock&#x2019;s notion of interactive programs in dependent type theory. The operators of CSP will be defined rather than atomic operations, and compute new ele-ments of the data type of processes from existing ones.The approach will make use of advanced type theoretic features: the use of inductive-recursively defined universes; the definition of coinductive types by their observations, which has similarities to the notion of an object in object-oriented programming; the use of sized types for coinductive types, which allow coinductive definitions in a modular way; the handling of fini-tary information (names of processes) in a coinductive settings; the use of named types for automatic inference of arguments similar to its use in tem-plate Meta-programming in C++; and the use of interactive programs in dependent type theory.We introduce a simulator as an interactive program in Agda. The simula-tor allows to observe the evolving of processes following external or internal choices. Our aim is to use this in order to simulate railway interlocking system and write programs in Agda which directly use CSP processes.Then we extend the trace semantics of CSP to the monadic setting. We implement this semantics, together with the corresponding refinement and equality relation, formally in CSP-Agda. In order to demonstrate the proof capabilities of CSP-Agda, we prove in CSP-Agda selected algebraic laws of CSP based on the trace semantics. Because of the monadic settings, some adjustments need to be made to these laws.Next we implement the more advanced semantics of CSP, the stable fail-ures semantics and the failures divergences infinite traces semantics (FDI), in CSP-Agda, and define the corresponding refinement and equality relations. Direct proofs in these semantics are cumbersome, and we develop a tech-nique of showing algebraic laws in those semantics in an indirect way, which is much easier. We introduce divergence-respecting weak bisimilarity and strong bisimilarity in CSP-Agda, and show that both imply equivalence with respect to stable failures and FDI semantics. Now we show certain algebraic laws with respect to one of these two bisimilarity relations. As a case study, we model and verify a possible scenario for railways in CSP-Agda and in standard CSP tools.</abstract><type>E-Thesis</type><journal/><publisher/><placeOfPublication>Swansea</placeOfPublication><keywords/><publishedDay>26</publishedDay><publishedMonth>4</publishedMonth><publishedYear>2018</publishedYear><publishedDate>2018-04-26</publishedDate><doi>10.23889/Suthesis.54270</doi><url/><notes/><college>COLLEGE NANME</college><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><supervisor>Setzer, Anton ; Berger, Ulrich</supervisor><degreelevel>Doctoral</degreelevel><degreename>Ph.D</degreename><apcterm/><lastEdited>2020-05-19T11:36:53.5964703</lastEdited><Created>2020-05-18T15:03:46.9190096</Created><authors><author><firstname>BASHAR</firstname><surname>ALKHAWALDEH</surname><order>1</order></author></authors><documents><document><filename>54270__17286__42c977b3ef4f420d89ba3edf602893cb.pdf</filename><originalFilename>Alkhawaldeh_Bashar_PhD_Thesis_Final.pdf</originalFilename><uploaded>2020-05-18T15:16:52.8636503</uploaded><type>Output</type><contentLength>3449409</contentLength><contentType>application/pdf</contentType><version>E-Thesis &#x2013; open access</version><cronfaStatus>true</cronfaStatus><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling 2020-05-19T11:36:53.5964703 v2 54270 2020-05-18 Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification 997fec2a691e4337ef78f7b096636ca1 BASHAR ALKHAWALDEH BASHAR ALKHAWALDEH true false 2020-05-18 We introduce a library called CSP-Agda for representing processes in the dependently typed theorem prover and interactive programming language Agda. We will enhance processes by a monad structure. The monad struc-ture facilitates combining processes in a modular way, and allows to define recursion as a direct operation on processes. Processes are defined coinduc-tively as non-well-founded trees. The nodes of the tree are formed by a an atomic one step relation, which determines for a process the external, internal choices, and termination events it can choose, and whether the process has terminated. The data type of processes is inspired by Setzer and Hancock’s notion of interactive programs in dependent type theory. The operators of CSP will be defined rather than atomic operations, and compute new ele-ments of the data type of processes from existing ones.The approach will make use of advanced type theoretic features: the use of inductive-recursively defined universes; the definition of coinductive types by their observations, which has similarities to the notion of an object in object-oriented programming; the use of sized types for coinductive types, which allow coinductive definitions in a modular way; the handling of fini-tary information (names of processes) in a coinductive settings; the use of named types for automatic inference of arguments similar to its use in tem-plate Meta-programming in C++; and the use of interactive programs in dependent type theory.We introduce a simulator as an interactive program in Agda. The simula-tor allows to observe the evolving of processes following external or internal choices. Our aim is to use this in order to simulate railway interlocking system and write programs in Agda which directly use CSP processes.Then we extend the trace semantics of CSP to the monadic setting. We implement this semantics, together with the corresponding refinement and equality relation, formally in CSP-Agda. In order to demonstrate the proof capabilities of CSP-Agda, we prove in CSP-Agda selected algebraic laws of CSP based on the trace semantics. Because of the monadic settings, some adjustments need to be made to these laws.Next we implement the more advanced semantics of CSP, the stable fail-ures semantics and the failures divergences infinite traces semantics (FDI), in CSP-Agda, and define the corresponding refinement and equality relations. Direct proofs in these semantics are cumbersome, and we develop a tech-nique of showing algebraic laws in those semantics in an indirect way, which is much easier. We introduce divergence-respecting weak bisimilarity and strong bisimilarity in CSP-Agda, and show that both imply equivalence with respect to stable failures and FDI semantics. Now we show certain algebraic laws with respect to one of these two bisimilarity relations. As a case study, we model and verify a possible scenario for railways in CSP-Agda and in standard CSP tools. E-Thesis Swansea 26 4 2018 2018-04-26 10.23889/Suthesis.54270 COLLEGE NANME COLLEGE CODE Swansea University Setzer, Anton ; Berger, Ulrich Doctoral Ph.D 2020-05-19T11:36:53.5964703 2020-05-18T15:03:46.9190096 BASHAR ALKHAWALDEH 1 54270__17286__42c977b3ef4f420d89ba3edf602893cb.pdf Alkhawaldeh_Bashar_PhD_Thesis_Final.pdf 2020-05-18T15:16:52.8636503 Output 3449409 application/pdf E-Thesis – open access true true eng
title Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification
spellingShingle Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification
BASHAR ALKHAWALDEH
title_short Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification
title_full Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification
title_fullStr Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification
title_full_unstemmed Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification
title_sort Integration of the Process Algebra CSP in Dependent Type Theory - Formalisation and Verification
author_id_str_mv 997fec2a691e4337ef78f7b096636ca1
author_id_fullname_str_mv 997fec2a691e4337ef78f7b096636ca1_***_BASHAR ALKHAWALDEH
author BASHAR ALKHAWALDEH
author2 BASHAR ALKHAWALDEH
format E-Thesis
publishDate 2018
institution Swansea University
doi_str_mv 10.23889/Suthesis.54270
document_store_str 1
active_str 0
description We introduce a library called CSP-Agda for representing processes in the dependently typed theorem prover and interactive programming language Agda. We will enhance processes by a monad structure. The monad struc-ture facilitates combining processes in a modular way, and allows to define recursion as a direct operation on processes. Processes are defined coinduc-tively as non-well-founded trees. The nodes of the tree are formed by a an atomic one step relation, which determines for a process the external, internal choices, and termination events it can choose, and whether the process has terminated. The data type of processes is inspired by Setzer and Hancock’s notion of interactive programs in dependent type theory. The operators of CSP will be defined rather than atomic operations, and compute new ele-ments of the data type of processes from existing ones.The approach will make use of advanced type theoretic features: the use of inductive-recursively defined universes; the definition of coinductive types by their observations, which has similarities to the notion of an object in object-oriented programming; the use of sized types for coinductive types, which allow coinductive definitions in a modular way; the handling of fini-tary information (names of processes) in a coinductive settings; the use of named types for automatic inference of arguments similar to its use in tem-plate Meta-programming in C++; and the use of interactive programs in dependent type theory.We introduce a simulator as an interactive program in Agda. The simula-tor allows to observe the evolving of processes following external or internal choices. Our aim is to use this in order to simulate railway interlocking system and write programs in Agda which directly use CSP processes.Then we extend the trace semantics of CSP to the monadic setting. We implement this semantics, together with the corresponding refinement and equality relation, formally in CSP-Agda. In order to demonstrate the proof capabilities of CSP-Agda, we prove in CSP-Agda selected algebraic laws of CSP based on the trace semantics. Because of the monadic settings, some adjustments need to be made to these laws.Next we implement the more advanced semantics of CSP, the stable fail-ures semantics and the failures divergences infinite traces semantics (FDI), in CSP-Agda, and define the corresponding refinement and equality relations. Direct proofs in these semantics are cumbersome, and we develop a tech-nique of showing algebraic laws in those semantics in an indirect way, which is much easier. We introduce divergence-respecting weak bisimilarity and strong bisimilarity in CSP-Agda, and show that both imply equivalence with respect to stable failures and FDI semantics. Now we show certain algebraic laws with respect to one of these two bisimilarity relations. As a case study, we model and verify a possible scenario for railways in CSP-Agda and in standard CSP tools.
published_date 2018-04-26T07:54:19Z
_version_ 1821391254347317248
score 11.047848

Similar Items