Abstract
Although liveness and fairness have been used for a long time in classical model checking, with process-algebraic methods they have seen far less use. One reason for this is that most well-known process-algebraic theories such as CSP and CCS have limited capability for handling liveness properties. In this article we discuss the problems and possibilities of liveness and fairness in process algebra. We show that most well-known semantic equivalences do not preserve enough fairness-related information and that fairness properties are difficult to combine with the bottom-up compositionality of process algebra. However, we also establish positive results for a useful subset of fairness properties. We develop a method that does not assume new fairness-related constructs or rules for processes, but uses the standard LTS model. We demonstrate the method by removing livelocks from a communication protocol.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alpern, B. & Schneider, F. “Defining Liveness”. Information Processing Letters, Vol. 21 (No. 4), 1985, North-Holland.
Apt, K., Francez, N. & Katz, S.: “Appraising fairness in languages for distributed programming”. Distributed Computing (1988) Vol. 2 (No. 4), Springer-Verlag, pp. 226–241.
Bartlett, K. A., Scantlebury, R. A. & Wilkinson, P. T.: “A Note on Reliable Full-Duplex Transmission Over Half-Duplex Links”, Communications of the ACM 12(5) 1969, pp. 260–261.
Bergstra, J. A., Klop, J. W.: “Verification of an Alternating Bit Protocol by Means of Process Algebra”. Mathematical Methods of Specification and Synthesis of Software Systems’ 85, Lecture Notes in Computer Science 215, Springer-Verlag 1985, pp. 9–23.
Brinksma, E., Rensink, A. & Vogler, W.: “Fair Testing”. CONCUR’95, Sixth International Conference on Concurrency Theory, Lecture Notes in Computer Science 962, Springer-Verlag 1995, pp. 313–327.
Clarke, E. M. & Emerson, E. A.: “Synthesis of Synchronization Skeletons for Branching Time Temporal Logic”. Proc. Logic in Programs: Workshop, 1981, Lecture Notes in Computer Science 131, Springer-Verlag 1981, pp. 52–71.
Cleaveland, R. & Lüttgen, G.: “A Semantic Theory for Heterogeneous System Design”. Proc. Foundations of Software Technology and Theoretical Computer Science 2000. Lecture Notes in Computer Science 1974, Springer-Verlag 2000, pp. 312–324.
Costa, G. & Stirling, C.: “A Fair Calculus of Communicating Systems”. Acta Informatica 21 (1984), Springer-Verlag, pp. 417–441.
Costa, G. & Stirling, C.: “Weak and Strong Fairness in CCS”. Proc. Mathematical Foundations of Computer Science 1984, Lecture Notes in Computer Science 176, Springer-Verlag 1984, pp. 245–254.
Davies, J. & Schneider, S.: “Using CSP to Verify a Timed Protocol over a Fair Medium”. Proc. CONCUR’92, Third International Conference on Concurrency Theory, Lecture Notes in Computer Science 630, Springer-Verlag 1992, pp. 355–369.
Francez, N.: “Fairness”. Springer-Verlag 1986, 295 p.
Hennessy, M.: “Axiomatising Finite Delay Operators”. Acta Informatica 21(1) 1984, Springer-Verlag, pp. 61–88.
Hennessy, M.: “An Algebraic Theory of Fair Asynchronous Communicating processes”. Theoretical Computer Science 49 (1987), North-Holland, pp. 121–143.
Kaivola, R. & Valmari, A.: “The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic”. Proc. CONCUR’ 92, Third International Conference on Concurrency Theory, Lecture Notes in Computer Science 630, Springer-Verlag 1992, pp. 207–221.
Lamport, L.: “Proving the Correctness of Multiprocess Programs”. IEEE Transactions on Software Engineering, Vol. SE-3 (No. 2) 1977, IEEE Computer Society, pp. 125–143.
Lamport, L.: “The Temporal Logic of Actions”. ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 16 (No. 3) 1994, pp. 872–923.
Lehmann, D., Pnueli, A. & Stavi, J.: “Impartiality, Justice and Fairness: The Ethics of Concurrent Termination”. Proc. Eighth International Colloquium on Automata, Languages and Programming 1981, Lecture Notes in Computer Science 115, Springer-Verlag 1981, pp. 264–277.
Manna, Z. & Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Volume I: Specification. Springer-Verlag 1992, 427 p.
Milner, R.: Communication and Concurrency. Prentice-Hall 1989, 260 p.
Parrow, J.: Fairness Properties in Process Algebra with Applications in Communication Protocol Verification. Ph.D. thesis, Uppsala University, Department of Computer Systems, 1985, 176 p.
Pnueli, A.: “A Temporal Logic of Concurrent Programs”. Theoretical Computer Science, 13, 1981, pp. 45–60.
Puhakka, A. & Valmari, A.: “Livelocks, Fairness and Protocol Verification”. Proc. World Computer Conference 2000, Conference on Software: Theory and Practice, International Federation for Information Processing (IFIP), pp. 471–479.
Puhakka, A. & Valmari, A.: “Liveness and Fairness in Process-Algebraic Verification”. To be published as Tampere University of Technology, Software Systems Laboratory Report 24, ISBN 952-15-0650-4.
Queille, J. P. & Sifakis, J.: “Specification and Verification of Concurrent Systems in CESAR”. Proc. Fifth International Symposium on Programming, 1981.
Roscoe, A. W.: The Theory and Practice of Concurrency. Prentice-Hall 1998, 565 p.
Valmari, A.: “Failure-based Equivalences Are Faster Than Many Believe”. Proc. Structures in Concurrency Theory 1995, Springer-Verlag “Workshops in Computing” series, 1995, pp. 326–340.
Valmari, A.: “Compositionality in State Space Verification Methods”. Proc. Application and Theory of Petri Nets 1996, Lecture Notes in Computer Science 1091, Springer-Verlag 1996, pp. 29–56.
Valmari, A., Kemppainen, J., Clegg, M. & Levanto, M.: “Putting Advanced Reachability Analysis Techniques Together: the ‘ARA’ Tool”. Proc. Formal Methods Europe’ 93, Lecture Notes in Computer Science 670, Springer-Verlag 1993, pp. 597–616.
Valmari, A. & Tienari, M.: “Compositional Failure-Based Semantic Models for Basic LOTOS”. Formal Aspects of Computing (1995) 7: 440–468.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Puhakka, A., Valmari, A. (2001). Liveness and Fairness in Process-Algebraic Verification. In: Larsen, K.G., Nielsen, M. (eds) CONCUR 2001 — Concurrency Theory. CONCUR 2001. Lecture Notes in Computer Science, vol 2154. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44685-0_14
Download citation
DOI: https://doi.org/10.1007/3-540-44685-0_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42497-0
Online ISBN: 978-3-540-44685-9
eBook Packages: Springer Book Archive