No Cover Image

E-Thesis 453 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!
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.
Keywords: Computer science.
College: Faculty of Science and Engineering

Similar Items