Temporal Property Preservation Under Z Refinement in CSP-OZ Specifications

Azman Bujang, Masli and Abdul Rahman, Mat and Suriati Khartini, Jali and Noor Hazlini, Borhan (2012) Temporal Property Preservation Under Z Refinement in CSP-OZ Specifications. International Conference on Computer & Information Science (ICCIS), 2012. ISSN ISBN: 978-1-4673-1938-6

[img]
Preview
PDF
Temporal Property Preservation Under Z Refinement(abstract).pdf

Download (209kB) | Preview

Abstract

One way to verify the correctness of an implementation under refinement in formal specifications is by verifying the system against a set of properties we wish to have in the final implementation. This is in such a way that the relevant properties are preserved in each development step. The difference here is that we have a separate specification of system properties. These properties are those that are satisfied by the initial specification. As the development of the system progresses from one step to another, the correctness of the concrete specification is verified by checking the satisfaction of the properties. The correctness of the abstract specification is preserved in the concrete specification (or an implementation) if the concrete specification satisfies all properties the abstract specification satisfies [1]. In other words, the properties are preserved and hold in the concrete specification. This paper extends the result on LTL property preservation for Z specifications in [2] to the OZ part of CSP-OZ specifications. This is where Z refinement exists side-by-side with CSP refinement in the CSP part of a CSP-OZ specification.

Item Type: Article
Uncontrolled Keywords: temporal logic, communicating sequential processes, formal specification, unimas, university, universiti, Borneo, Malaysia, Sarawak, Kuching, Samarahan, ipta, education, research, Universiti Malaysia Sarawak
Subjects: T Technology > T Technology (General)
Divisions: Academic Faculties, Institutes and Centres > Faculty of Computer Science and Information Technology
Depositing User: Karen Kornalius
Date Deposited: 12 Jun 2017 04:39
Last Modified: 12 Jun 2017 04:39
URI: http://ir.unimas.my/id/eprint/16599

Actions (For repository members only: login required)

View Item View Item