Designing CSP-OZ Transitivity Property Using Formal Specification

• Main Author: Suresh, Ramachandran
• Format: Thesis
• Language: English
• Published: Universiti Malaysia Sarawak (UNIMAS) 2019
• Subjects: QA76 Computer software; T201 Patents. Trademarks
• Online Access: http://ir.unimas.my/id/eprint/27674/1/Suresh.pdf; http://ir.unimas.my/id/eprint/27674/

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