Temporal-logic property preservation under Z refinement |
| |
Authors: | John Derrick Graeme Smith |
| |
Affiliation: | 1. Department of Computer Science, University of Sheffield, Sheffield, UK 2. School of Information Technology and Electrical Engineering, The University of Queensland, Brisbane, 4072, Australia
|
| |
Abstract: | Formal specification languages such as Z, B and VDM are used in the incremental development of abstract specifications (suitable
for establishing required properties) to more concrete specifications (resembling the final implementation). This incremental
development process, known as refinement, preserves all observable properties of the original abstract specification. Recent research has looked at applying temporal-logic
model checking to such specification languages. While this assists in the establishment of properties of the abstract specification,
temporal-logic properties typically refer to state variables which are regarded as non-observable. Hence, such properties
are not guaranteed to be preserved by refinement. This paper investigates the classes of temporal-logic properties which are
preserved by refinement, and for some of those properties that are not preserved in general, the restrictions on the refinement
process under which they are preserved. Results are presented for the temporal logics LTL, CTL and the μ-calculus and the formal specification language Z. They apply equally, however, to related formal specification languages
such as B and VDM. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|