Abstract
To facilitate the construction of concurrent programs based on progress requirements, we study an integration of the Owicki/Gries theory with UNITY’s leads-to relation. In particular we investigate a set of calculational rules for leads-to, and we study the composition of programs regarding their effect on progress. Apart from parallel composition, we consider the less familiar notion of weak sequential composition. Our techniques are illustrated on two network initialisation protocols that are related to the protocol standard IEEE 1394.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Collette, P., Knapp, E.: A foundation for modular reasoning about safety and progress properties of state-based concurrent programs. Theoretical Computer Science 183, 253–279 (1997)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley Longman Publishing Co. Inc., Reading (1988)
Dongol, B., Goldson, D.: Extending the theory of Owicki and Gries with a logic of progress. Logical Methods in Computer Science 2(1), 1–25 (2006)
Devillers, M.C.A., Griffioen, W.O.D., Romijn, J.M.T., Vaandrager, F.W.: Verification of a leader election protocol – formal methods applied to IEEE 1394. Formal methods in system design 16(3), 307–320 (2000)
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Dongol, B., Mooij, A.J.: Progress in deriving concurrent programs: emphasizing the role of stable guards. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 140–161. Springer, Heidelberg (2006)
Dongol, B., Mooij, A.J.: Streamlining progress-based derivations of concurrent programs. Technical Report SSE-2006-06, School of Information Technology and Electrical Engineering, The University of Queensland, 2006. Accepted for publication in the Formal Aspects of Computing journal (2006)
Dongol, B.: Formalising progress properties of non-blocking programs. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 284–303. Springer, Heidelberg (2006)
Fokkink, W., Groote, J.F., Reniers, M.A.: Process algebra needs proof methodology. In: Aceto, L. (ed.) The concurrency column. Bulletin of the EATCS, vol. 82, pp. 108–125 (February 2004)
Feijen, W.H.J., van Gasteren, A.J.M.: On a method of multiprogramming. Springer, Heidelberg (1999)
Hoogerwoord, R.R.: A formal derivation of a sliding window protocol. Computer Science Report 06-31, Technische Universiteit Eindhoven (2006)
Institute of Electrical and Electronics Engineers. IEEE standard for a high performance serial bus, IEEE Std 1394-1995 (August 1996)
Institute of Electrical and Electronics Engineers. IEEE standard for high performance serial bus bridges, IEEE Std 1394.1-2004 (July 2005)
International Telecommunication Union - Telecom Standardization. Message Sequence Chart, ITU-T Recommendation Z.120 (2000)
Jones, C.B.: Development methods for computer programs including a notion of interference, Oxford University Computing Laboratory. Dphil. thesis (1981)
Knapp, E.: Derivation of concurrent programs: two examples. Science of Computer Programming 19(1), 1–23 (1992)
Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)
Misra, J.: Phase synchronization. Information Processing Letters 38(2), 101–105 (1991)
Misra, J.: A logic for concurrent programming. Technical report, The University of Texas at Austin (April 1994)
Mooij, A.J.: Constructive formal methods and protocol standardization, Technische Universiteit Eindhoven, PhD thesis (October 2006)
Mooij, A.J.: Constructing and reasoning about security protocols using invariants. In: REFINE 2007. ENTCS (to appear, 2007)
Manna, Z., Pnueli, A.: Completing the temporal picture. Theoretical Computer Science 83(1), 91–130 (1991)
Mooij, A.J., Wesselink, J.W.: A formal analysis of a dynamic distributed spanning tree algorithm. Computer Science Report 03-16, Technische Universiteit Eindhoven (2003)
Mooij, A.J., Wesselink, J.W.: Incremental verification of Owicki/Gries proof outlines using PVS. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 390–404. Springer, Heidelberg (2005)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319–340 (1976)
Prasetya, I.S.W.B., Vos, T.E.J., Azurat, A., Swierstra, S.D.: A UNITY-based framework towards component based systems. In: Higashino, T. (ed.) OPODIS 2004. LNCS, vol. 3544, pp. 52–66. Springer, Heidelberg (2005)
Romijn, J., Wesselink, W., Mooij, A.: Assertion-based proof checking of Chang-Roberts leader election in PVS. In: Mamjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) TSDM 2000. LNCS, vol. 4762, Springer, Heidelberg (2007)
Stolen, K.: A method for the development of totally correct shared-state parallel programs. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol. 527, pp. 510–525. Springer, Heidelberg (1991)
Xu, Q., de Roever, W.-P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 149–174 (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mooij, A.J. (2007). Calculating and Composing Progress Properties in Terms of the Leads-to Relation. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds) Formal Methods and Software Engineering. ICFEM 2007. Lecture Notes in Computer Science, vol 4789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-76650-6_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-76650-6_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-76648-3
Online ISBN: 978-3-540-76650-6
eBook Packages: Computer ScienceComputer Science (R0)