Designing CSP-OZ Transitivity Property Using Formal Specification

A formal specification language provides a technique to describe a system’s behaviour and its properties. The initial specification is abstract which needs to be transformed to a concrete specification using refinement process. In integrated formal specification, the specification is a combination o...

Full description

Saved in:

Bibliographic Details
Main Author:	Suresh, Ramachandran
Format:	Thesis
Language:	English
Published:	2019
Subjects:	QA76 Computer software
Online Access:	http://ir.unimas.my/id/eprint/27674/1/Suresh.pdf
Tags:	Add Tag No Tags, Be the first to tag this record!

id	my-unimas-ir.27674
record_format	uketd_dc
spelling	my-unimas-ir.276742023-07-06T07:11:15Z Designing CSP-OZ Transitivity Property Using Formal Specification 2019-09-15 Suresh, Ramachandran QA76 Computer software T201 Patents. Trademarks A formal specification language provides a technique to describe a system’s behaviour and its properties. The initial specification is abstract which needs to be transformed to a concrete specification using refinement process. In integrated formal specification, the specification is a combination of state-based and event-based specification. Hence, two or more types of refinement behaviour exists in integrated formal specification. This research focuses on CSP OZ specification as it comprises both event-based (CSP) and state-based (OZ) specifications. During refinement, the CSP refinement removes the non-determinism behaviour of CSP while the OZ refinement is required to make OZ concrete specification. These restrict the proving of transitivity property in CSP-OZ as the refinements involve two different refinement processes. Moreover, the CSP and OZ does not share same semantic definitions. The objectives of this research are to develop a formal specification, to design a theory to prove the existence of transitivity property in CSP-OZ, and to apply the theory in formal specification. The syntax and semantics of CSP, OZ, and CSP-OZ were studied before identifying the suitable CSP-OZ semantics to execute the proving process. To prove refinement property, the CSP-OZ must define into single semantics definitions. Here, the approach of converting of the both CSP and OZ parts to a single semantics is applied. The successfully converted semantics are continue with the proving process. The proving model are created based the definition of refinement process where it states that the refined specification must equal or subset to the abstract specification. The theory is test with a simpler example. Then, a case study was built to implement and verify the result and outcomes. The case study is designed based the rural area requirement. The result shows as expected which is the existence of the transitivity property is proven using labelled transition system, relational semantics and failure semantics. Keywords: Refinement property, transitivity property, multiple refinement, integrated formal specification, semantics Universiti Malaysia Sarawak (UNIMAS) 2019-09 Thesis http://ir.unimas.my/id/eprint/27674/ http://ir.unimas.my/id/eprint/27674/1/Suresh.pdf text en validuser masters Universiti Malaysia Sarawak (UNIMAS) Faculty of Computer Science and Information Technology
institution	Universiti Malaysia Sarawak
collection	UNIMAS Institutional Repository
language	English
topic	QA76 Computer software QA76 Computer software
spellingShingle	QA76 Computer software QA76 Computer software Suresh, Ramachandran Designing CSP-OZ Transitivity Property Using Formal Specification
description	A formal specification language provides a technique to describe a system’s behaviour and its properties. The initial specification is abstract which needs to be transformed to a concrete specification using refinement process. In integrated formal specification, the specification is a combination of state-based and event-based specification. Hence, two or more types of refinement behaviour exists in integrated formal specification. This research focuses on CSP OZ specification as it comprises both event-based (CSP) and state-based (OZ) specifications. During refinement, the CSP refinement removes the non-determinism behaviour of CSP while the OZ refinement is required to make OZ concrete specification. These restrict the proving of transitivity property in CSP-OZ as the refinements involve two different refinement processes. Moreover, the CSP and OZ does not share same semantic definitions. The objectives of this research are to develop a formal specification, to design a theory to prove the existence of transitivity property in CSP-OZ, and to apply the theory in formal specification. The syntax and semantics of CSP, OZ, and CSP-OZ were studied before identifying the suitable CSP-OZ semantics to execute the proving process. To prove refinement property, the CSP-OZ must define into single semantics definitions. Here, the approach of converting of the both CSP and OZ parts to a single semantics is applied. The successfully converted semantics are continue with the proving process. The proving model are created based the definition of refinement process where it states that the refined specification must equal or subset to the abstract specification. The theory is test with a simpler example. Then, a case study was built to implement and verify the result and outcomes. The case study is designed based the rural area requirement. The result shows as expected which is the existence of the transitivity property is proven using labelled transition system, relational semantics and failure semantics. Keywords: Refinement property, transitivity property, multiple refinement, integrated formal specification, semantics
format	Thesis
qualification_level	Master's degree
author	Suresh, Ramachandran
author_facet	Suresh, Ramachandran
author_sort	Suresh, Ramachandran
title	Designing CSP-OZ Transitivity Property Using Formal Specification
title_short	Designing CSP-OZ Transitivity Property Using Formal Specification
title_full	Designing CSP-OZ Transitivity Property Using Formal Specification
title_fullStr	Designing CSP-OZ Transitivity Property Using Formal Specification
title_full_unstemmed	Designing CSP-OZ Transitivity Property Using Formal Specification
title_sort	designing csp-oz transitivity property using formal specification
granting_institution	Universiti Malaysia Sarawak (UNIMAS)
granting_department	Faculty of Computer Science and Information Technology
publishDate	2019
url	http://ir.unimas.my/id/eprint/27674/1/Suresh.pdf
_version_	1783728350524604416

Designing CSP-OZ Transitivity Property Using Formal Specification

Similar Items