Abstract
This paper presents a novel application of an untimed process algebra formalism to a class of timing-critical verification problems usually modelled with either timed automata or timed process algebra. We show that a formalism based on interacting automata can model system components, behavioural constraints and properties requiring proof without elaborating the underlying process-algebraic formalism to include explicit timing constructs; and that properties can be verified without introducing temporal logic, model-checking, or refinement relation checking. We demonstrate this technique in detail by application to the Fischer mutual-exclusion protocol, an archetypal example of a system that depends of timing constraints to operate correctly.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Lamport, L.: Conjoining specifications. ACM Transactions on Programming Languages 17(3) (1995)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Ammerlaan, M., Spelberg, R.L., Toetenel, H.: XTG - an engineering approach to modelling and analysis of real-time systems. In: 10th Euromicro Workshop on Real Time Systems, pp. 88–97. IEEE Computer Society Press, Los Alamitos (1998)
Cerone, A., Cowie, A.J., Milne, G.J., Moseley, P.A.: Modelling a time-dependant protocol using the CIRCAL process algebra. LNCS, vol. 2102, pp. 124–138 (1997)
Cerone, A., Kearney, D.A., Milne, G.J.: Integrating the verification of timing, performance and correctness properties of concurrent systems. In: The International Conference on Application of Concurrency to System Design, pp. 109–119. IEEE Computer Society Press, Los Alamitos (1998)
Cerone, A., Milne, G.J.: A methodology for the formal analysis of asynchronous micropipelines. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 246–262. Springer, Heidelberg (2000)
Cowie, A.: The Modelling of Temporal Properties in a Process Algebra Framework. PhD thesis, University of South Australia (1999)
Furber, S.B., Day, P.: Four-phase micropipeline latch control circuit. IEEE Transactions on VLSI Systems 4(2), 247–253 (1996)
Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1985)
Kelso, J.: Proof of the soundness of the concurrent composition property checking technique. Technical Report Report-05-003, School of Computer Science and Software Engineering, Univeristy of Western Australia (2005)
Kelso, J., Milne, G.: The prototype Haskell CIRCAL system (2003), http://www.csse.uwa.edu.au/FormalSpecification/HaskellCircal/
Kelso, J., Milne, G.: An interacting automata model of a fault-tolerant scada system. Technical Report Report-05-004, School of Computer Science and Software Engineering, Univeristy of Western Australia (2005)
Knuth, D.E., Morris, J.H., Pratt, V.R.: Fast pattern matching in strings. SIAM Journal on Computing 6(1), 323–350 (1997)
Kristoffersen, K.J., Laroussinie, F., Larsen, K.G., Pettersson, P., Yi, W.: A composition proof of a real-time mutual exclusion protocol. Technical Report RS-96-55, Aalborg University, Denmark (1996)
Lamport, L.: A fast mutual exclusion algorithm. ACM Transactions on Computer Systems 5(1), 1–11 (1987)
Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems 16(3), 872–923 (1994)
Milne, G.J.: CIRCAL and the representation of communication, concurrency and time. ACM Transactions on Programming Languages and Systems 7(2), 270–298 (1985)
Milne, G.J.: Formal Specification and Verification of Digital Systems. McGraw-Hill, New York (1994)
Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1989)
Nicollin, X., Sifakis, J.: An overview and synthesis on timed process algebras. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 376–398. Springer, Heidelberg (1992)
Plotkin, G.: Structural operational semantics. Technical Report DAIMI FN-19, Aahus University (1981) (reprinted in 1991)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs (1997)
Sutherland, I.E.: Micropipelines. Communications of the ACM 32(6), 720–738 (1989)
Vereijken, J.: Fischer’s protocol in timed process algebra. Technical Report CSR 94/32, Eindhoven University of Technology, Computing Science Department (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 IFIP International Federation for Information Processing
About this paper
Cite this paper
Kelso, J., Milne, G. (2005). Properties as Processes: Their Specification and Verification. In: Wang, F. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2005. FORTE 2005. Lecture Notes in Computer Science, vol 3731. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562436_36
Download citation
DOI: https://doi.org/10.1007/11562436_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29189-3
Online ISBN: 978-3-540-32084-5
eBook Packages: Computer ScienceComputer Science (R0)