Abstract
This paper studies the laws of communicating sequential processes (CSP) with Z-like initial and final states. Instead of defining a large semantics including all observable aspects, we incrementally develop the model in three stages: partially correct relational model, then totally correct sequential model and finally the reactive-process model with states. The properties of each model are captured as algebraic laws. A law in one model may or may not be true in its submodels. We apply a technique based on healthiness conditions to identify the conditions for law inheritance. Such abstract conditions themselves can be captured as pattern laws of commutativity. The model uses a new approach to define parallel compositions using just the primitive commands, nondeterministic choice, conjunction and some unary (hiding) operators.
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.
Similar content being viewed by others
References
Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, pp. 1–168. Oxford University Press, New York (1994)
Back, R.J., von Wright, J.: Trace refinement of action systems. In: International Conference on Concurrency Theory, pp. 367–384 (1994)
Butler, M.: A CSP Approach To Action Systems. PhD thesis, OUCL, University of Oxford, Oxford (1992)
Cavalcanti, A., Woodcock, J.: Predicate transformers in the semantics of Circus. IEE Proceedings - Software 150(2), 85–94 (2003)
Chen, Y.: Generic composition. Formal Aspects of Computing 14(2), 108–122 (2002)
Chen, Y.: Hierarchical organisation of predicate-semantic models. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 155–172. Springer, Heidelberg (2006)
Chen, Y.: Sharing properties between programming models. Technical report, Department of Computer Science, Durham University (2007)
Chen, Y., Sanders, J.W.: Logic of global synchrony. ACM Transactions on Programming Languages and Systems 26(2), 221–262 (2004)
Dijkstra, E.W.: Guarded commands, nondeterminacy and the formal derivation of programs. Communications of the ACM 18(8), 453–457 (1975)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Hoare, C.A.R.: Dicussions about parallel composition as conjunction. Private communication (2006)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)
Morgan, C.C.: Beauty is our business: a birthday salute to Edsger W. Dijkstra, chapter Of wp and CSP, pp. 319–326. Springer, Heidelberg (1990)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)
Schneider, S., Treharne, H.: Verifying controlled components. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 87–107. Springer, Heidelberg (2004)
Zhou, J., Chen, Y.: Generating C code from LOGS specifications. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 195–210. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, Y. (2007). Inheriting Laws for Processes with States. In: Davies, J., Gibbons, J. (eds) Integrated Formal Methods. IFM 2007. Lecture Notes in Computer Science, vol 4591. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73210-5_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-73210-5_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73209-9
Online ISBN: 978-3-540-73210-5
eBook Packages: Computer ScienceComputer Science (R0)