Cover Image

Temporal Property Preservation Under Z Refinement in CSP-OZ Specifications

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 differen...

Full description

Saved in:
Bibliographic Details
Main Authors: Azman Bujang, Masli, Abdul Rahman, Mat, Suriati Khartini, Jali, Noor Hazlini, Borhan
Format: E-Article
Language:English
Published: IEEE 2012
Subjects:
T Technology (General)
Online Access:http://ir.unimas.my/id/eprint/16599/1/Temporal%20Property%20Preservation%20Under%20Z%20Refinement%28abstract%29.pdf
http://ir.unimas.my/id/eprint/16599/
http://ieeexplore.ieee.org/document/6297152/
Tags: Add Tag
No Tags, Be the first to tag this record!
id my.unimas.ir.16599
record_format eprints
spelling my.unimas.ir.165992017-06-12T04:39:16Z http://ir.unimas.my/id/eprint/16599/ Temporal Property Preservation Under Z Refinement in CSP-OZ Specifications Azman Bujang, Masli Abdul Rahman, Mat Suriati Khartini, Jali Noor Hazlini, Borhan T Technology (General) 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. IEEE 2012 E-Article PeerReviewed text en http://ir.unimas.my/id/eprint/16599/1/Temporal%20Property%20Preservation%20Under%20Z%20Refinement%28abstract%29.pdf 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 http://ieeexplore.ieee.org/document/6297152/ 10.1109/ICCISci.2012.6297152
institution Universiti Malaysia Sarawak
building Centre for Academic Information Services (CAIS)
collection Institutional Repository
continent Asia
country Malaysia
content_provider Universiti Malaysia Sarawak
content_source UNIMAS Institutional Repository
url_provider http://ir.unimas.my/
language English
topic T Technology (General)
spellingShingle T Technology (General)
Azman Bujang, Masli
Abdul Rahman, Mat
Suriati Khartini, Jali
Noor Hazlini, Borhan
Temporal Property Preservation Under Z Refinement in CSP-OZ Specifications
description 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.
format E-Article
author Azman Bujang, Masli
Abdul Rahman, Mat
Suriati Khartini, Jali
Noor Hazlini, Borhan
author_facet Azman Bujang, Masli
Abdul Rahman, Mat
Suriati Khartini, Jali
Noor Hazlini, Borhan
author_sort Azman Bujang, Masli
title Temporal Property Preservation Under Z Refinement in CSP-OZ Specifications
title_short Temporal Property Preservation Under Z Refinement in CSP-OZ Specifications
title_full Temporal Property Preservation Under Z Refinement in CSP-OZ Specifications
title_fullStr Temporal Property Preservation Under Z Refinement in CSP-OZ Specifications
title_full_unstemmed Temporal Property Preservation Under Z Refinement in CSP-OZ Specifications
title_sort temporal property preservation under z refinement in csp-oz specifications
publisher IEEE
publishDate 2012
url http://ir.unimas.my/id/eprint/16599/1/Temporal%20Property%20Preservation%20Under%20Z%20Refinement%28abstract%29.pdf
http://ir.unimas.my/id/eprint/16599/
http://ieeexplore.ieee.org/document/6297152/
_version_ 1644512410738884608
score 13.223943

Similar Items