Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10329380 | Electronic Notes in Theoretical Computer Science | 2005 | 18 Pages |
Abstract
Proofs about system specifications are difficult to conduct, particularly for large specifications. Using abstraction and refinement, we propose a proof technique that simplifies these proofs. We apply the technique to Circus (a combination of Z and CSP) specifications of different complexities. Interestingly, all the proofs are conducted in Z, even those concerning reactive behaviour.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
D. Atiya, S. King, J.C.P. Woodcock,