No Cover Image

E-Thesis 342 views 245 downloads

Property preserving development and testing for CSP-CASL. / TEMESGHEN AZENE

Swansea University Author: TEMESGHEN AZENE

Abstract

This thesis describes a theoretical study and an industrial application in the area of formal systems development, verification and formal testing using the specification language CSP-CASL. The latter is a comprehensive specification language which allows to describe systems in a combined algebraic...

Full description

Published: 2009
Institution: Swansea University
Degree level: Doctoral
Degree name: Ph.D
URI: https://cronfa.swan.ac.uk/Record/cronfa42217
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2018-08-02T18:54:10Z
last_indexed 2020-09-04T03:03:02Z
id cronfa42217
recordtype RisThesis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2020-09-03T09:01:28.6956193</datestamp><bib-version>v2</bib-version><id>42217</id><entry>2018-08-02</entry><title>Property preserving development and testing for CSP-CASL.</title><swanseaauthors><author><sid>c0d8121787aa27765d36aca3fd1d79a4</sid><firstname>TEMESGHEN</firstname><surname>AZENE</surname><name>TEMESGHEN AZENE</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2018-08-02</date><abstract>This thesis describes a theoretical study and an industrial application in the area of formal systems development, verification and formal testing using the specification language CSP-CASL. The latter is a comprehensive specification language which allows to describe systems in a combined algebraic / process algebraic notation. To this end it integrates the process algebra CSP and the algebraic specification language CASL. In this thesis we propose various formal development notions for CSP-CASL capable of capturing informal vertical and horizontal software development which we typically find in industrial applications. We provide proof techniques for such development notions and verification methodologies to prove interesting properties of reactive systems. We also propose a theoretical framework for formal testing from CSP-CASL specifications. Here, we present a conformance relation between a physical system and a CSP-C ASL specification. In particular we study the relationship between CSP-CASL development notions and the implemented system. The proposed theoretical notions of formal system development, property verification and formal testing for CSP-CASL, have been successfully applied to two industrial application: an electronic payment system called EP2 and the starting system of the BR725 Rolls- Royce jet engine control software.</abstract><type>E-Thesis</type><journal/><publisher/><keywords>Computer science.</keywords><publishedDay>31</publishedDay><publishedMonth>12</publishedMonth><publishedYear>2009</publishedYear><publishedDate>2009-12-31</publishedDate><doi/><url/><notes/><college>COLLEGE NANME</college><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><degreelevel>Doctoral</degreelevel><degreename>Ph.D</degreename><apcterm/><lastEdited>2020-09-03T09:01:28.6956193</lastEdited><Created>2018-08-02T16:24:28.4641899</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>TEMESGHEN</firstname><surname>AZENE</surname><order>1</order></author></authors><documents><document><filename>0042217-02082018162437.pdf</filename><originalFilename>10797919.pdf</originalFilename><uploaded>2018-08-02T16:24:37.2930000</uploaded><type>Output</type><contentLength>12773647</contentLength><contentType>application/pdf</contentType><version>E-Thesis</version><cronfaStatus>true</cronfaStatus><embargoDate>2018-08-02T00:00:00.0000000</embargoDate><copyrightCorrect>false</copyrightCorrect></document></documents><OutputDurs/></rfc1807>
spelling 2020-09-03T09:01:28.6956193 v2 42217 2018-08-02 Property preserving development and testing for CSP-CASL. c0d8121787aa27765d36aca3fd1d79a4 TEMESGHEN AZENE TEMESGHEN AZENE true false 2018-08-02 This thesis describes a theoretical study and an industrial application in the area of formal systems development, verification and formal testing using the specification language CSP-CASL. The latter is a comprehensive specification language which allows to describe systems in a combined algebraic / process algebraic notation. To this end it integrates the process algebra CSP and the algebraic specification language CASL. In this thesis we propose various formal development notions for CSP-CASL capable of capturing informal vertical and horizontal software development which we typically find in industrial applications. We provide proof techniques for such development notions and verification methodologies to prove interesting properties of reactive systems. We also propose a theoretical framework for formal testing from CSP-CASL specifications. Here, we present a conformance relation between a physical system and a CSP-C ASL specification. In particular we study the relationship between CSP-CASL development notions and the implemented system. The proposed theoretical notions of formal system development, property verification and formal testing for CSP-CASL, have been successfully applied to two industrial application: an electronic payment system called EP2 and the starting system of the BR725 Rolls- Royce jet engine control software. E-Thesis Computer science. 31 12 2009 2009-12-31 COLLEGE NANME COLLEGE CODE Swansea University Doctoral Ph.D 2020-09-03T09:01:28.6956193 2018-08-02T16:24:28.4641899 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science TEMESGHEN AZENE 1 0042217-02082018162437.pdf 10797919.pdf 2018-08-02T16:24:37.2930000 Output 12773647 application/pdf E-Thesis true 2018-08-02T00:00:00.0000000 false
title Property preserving development and testing for CSP-CASL.
spellingShingle Property preserving development and testing for CSP-CASL.
TEMESGHEN AZENE
title_short Property preserving development and testing for CSP-CASL.
title_full Property preserving development and testing for CSP-CASL.
title_fullStr Property preserving development and testing for CSP-CASL.
title_full_unstemmed Property preserving development and testing for CSP-CASL.
title_sort Property preserving development and testing for CSP-CASL.
author_id_str_mv c0d8121787aa27765d36aca3fd1d79a4
author_id_fullname_str_mv c0d8121787aa27765d36aca3fd1d79a4_***_TEMESGHEN AZENE
author TEMESGHEN AZENE
author2 TEMESGHEN AZENE
format E-Thesis
publishDate 2009
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 This thesis describes a theoretical study and an industrial application in the area of formal systems development, verification and formal testing using the specification language CSP-CASL. The latter is a comprehensive specification language which allows to describe systems in a combined algebraic / process algebraic notation. To this end it integrates the process algebra CSP and the algebraic specification language CASL. In this thesis we propose various formal development notions for CSP-CASL capable of capturing informal vertical and horizontal software development which we typically find in industrial applications. We provide proof techniques for such development notions and verification methodologies to prove interesting properties of reactive systems. We also propose a theoretical framework for formal testing from CSP-CASL specifications. Here, we present a conformance relation between a physical system and a CSP-C ASL specification. In particular we study the relationship between CSP-CASL development notions and the implemented system. The proposed theoretical notions of formal system development, property verification and formal testing for CSP-CASL, have been successfully applied to two industrial application: an electronic payment system called EP2 and the starting system of the BR725 Rolls- Royce jet engine control software.
published_date 2009-12-31T03:52:32Z
_version_ 1763752597085224960
score 11.035655

Similar Items