Open AccessSimpler Reasoning About System Properties: a Proof-by-Refinement Technique
Author(s) -
Diyaa-Addein Atiya,
S. King,
Jim Woodcock
Publication year - 2005
Publication title -
electronic notes in theoretical computer science
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.242
H-Index - 60
ISSN - 1571-0661
DOI - 10.1016/j.entcs.2005.04.022
Subject(s) - mathematical proof , abstraction , computer science , proof complexity , programming language , proof theory , automated proof checking , theoretical computer science , calculus (dental) , automated theorem proving , algorithm , mathematics , medicine , philosophy , geometry , dentistry , epistemology
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
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom