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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Aceto L, Ingólfsdóttir A (1999) Testing Hennessy–Milner logic with recursion. In: Foundations of software science and computation structure, pp 41–55
Boudol G, Larsen KG (1992) Graphical versus logical specifications. Theor Comput Sci 106(1):3–20
Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244–263
Hennessy M, Milner R (1985) Algebraic laws for nondeterminism and concurrency. J ACM 32:137–161
Hoare CAR (1985) Communicating sequential processes. Prentice Hall, Englewood Cliffs
Holzmann G (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5):279–295
Holzmann G (2003) The SPIN model checker. Addison-Wesley, Reading
Jackson D (1992) Logic verification of reactive software systems. D. Phil thesis, Oxford University
Leuschel M, Massart T, Currie A (2001) How to make FDR spin: LTL model checking of CSP by refinement. In: Proceedings of formal methods Europe FME’2001, LNCS 2021. Springer, Heidelberg, pp 99–118
Lowe G (1998) Casper: A compiler for the analysis of security protocols. J Comput Secur 6:53–84
Mukarram A (1993) A refusal testing model for CSP. D. Phil thesis, Oxford
Phillips I (1987) Refusal testing. Theor Comput Sci 50:241–284
Pnueli A (1981) The temporal logic of concurrent programs. Theor Comput Sci 13:45–60
Roscoe AW (1994) Model-checking CSP. In: A classical mind, essays in honour of C.A.R. Hoare. Prentice-Hall, Englewood Cliffs
Roscoe AW (1997) The theory and practice of concurrency. Prentice Hall, Englewood Cliffs
Roscoe AW (2005) On the expressive power of CSP refinement. Form Aspects Comput 17(2):93–112
Syverson P, Meadows C (1996) A formal language for cryptographic protocol requirements. Des Codes Cryptogr 7(1,2):27–59
Vardi M, Wolper P (1986) An automata-theoretic approach to automatic program validation. In: Proceedings of LICS’86, pp 332–344
Wolper P (1983) Temporal logic can be more expressive. Inf Control 56(1–2):72–99
Wolper P (2001) Constructing automata from temporal logic formulas: A tutorial. In: Lectures on formal methods in performance analysis (First EEF/Euro Summer School on Trends in Computer Science), LNCS 2090. Springer, Heidelberg, pp 261–277
Zakiuddin I, Moffat N, Goldsmith M, Whitworth T (2002) Property based compression strategies. In: Proceedings of the second workshop on automated verification of critical systems (AVoCS 2002)
Author information
Authors and Affiliations
Corresponding author
Additional information
M. J. Butler
Rights and permissions
About this article
Cite this article
Lowe, G. Specification of communicating processes: temporal logic versus refusals-based refinement. Form Asp Comp 20, 277–294 (2008). https://doi.org/10.1007/s00165-007-0065-0
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-007-0065-0