Specification of communicating processes: temporal logic versus refusals-based refinement |
| |
Authors: | Gavin Lowe |
| |
Affiliation: | (1) Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK |
| |
Abstract: | In this paper we consider the relationship between refinement-oriented specification and specifications using a temporal logic.
We investigate the extent to which one can check whether a program in a process algebra, such as Communicating Sequential
Processes (CSP), satisfies a temporal logic specification using a refinement-based model checker, such as FDR. We consider
what atomic formulae are appropriate in a temporal logic for specifying communicating processes, in particular where one wants
to talk about the availability of events. We then show that, perhaps surprisingly, the standard stable failures model is not
adequate for capturing specifications in such a logic: instead the refusal traces model must be used. We formalise the logic
by giving it a semantics in this model. We show that the temporal operators eventually and until, and negation, cannot, in general, be tested for via simple refinement checks. For the remaining fragment of the logic, we
present a translation into simple refinement checks. Finally, we show that refusal traces equivalence is characterised by
a slightly augmented version of that fragment.
M. J. Butler |
| |
Keywords: | Temporal logic Specification Refinement testing Refusals CSP |
本文献已被 SpringerLink 等数据库收录! |
|