Refinement in integrated specifications of CSP-OZ
Formal specification provides the means to verify a system's correctness and this can be done by the development technique of refinement of formal specification. Considering the multiple views of a system, in integrated formal specifications, will introduce more than one refinement that can be...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Institute of Electrical and Electronics Engineers
2015
|
| Subjects: | |
| Online Access: | http://ir.unimas.my/id/eprint/15210/2/Refinement.pdf http://ir.unimas.my/id/eprint/15210/ https://www.scopus.com/inward/record.uri?eid=2-s2.0-84962050760&doi=10.1109%2fICSECS.2015.7333098&partnerID=40&md5=80cb2d56d28953297b3dc0d93f45f383 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | Formal specification provides the means to verify a system's correctness and this can be done by the development technique of refinement of formal specification. Considering the multiple views of a system, in integrated formal specifications, will introduce more than one refinement that can be applied to the specification. This paper investigates the interaction of the different parts of an integrated specification under refinement. The integrated notation of CSP-OZ integrates the behaviour based language CSP with the state based notation, Object-Z. In such integrated notation, not only different views of a system are available, but the refinement relations in both parts are also of different basis. |
|---|