Simulating truly concurrent CSP. (English) Zbl 1325.68160

Davies, Jim (ed.) et al., Formal methods: foundations and applications. 13th Brazilian symposium on formal methods, SBMF 2010, Natal, Brazil, November 8–11, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-19828-1/pbk). Lecture Notes in Computer Science 6527, 128-143 (2011).
Summary: Process algebras like CSP provide a convenient intermediate-level formalism for the design of concurrent systems by allowing processes to be combined in parallel in such a way that the designer abstracts synchronization mechanisms and simultaneity of events. However some purposes require potential simultaneity to be made explicit. One approach is to produce new semantics models encapsulating that information. The approach taken here is to use the standard models and the CSP tool, FDR, to simulate a process in such a way to reveal potentially simultaneous events. The simulation is achieved by a construction that splits events into start and end events and monitors the result in a manner faithful to the original process. The method is applied to determine pairs of possibly concurrent events and to compute maximal simultaneity in a CSP design.
For the entire collection see [Zbl 1213.68032].


68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)


FDR2; CSP-prover
Full Text: DOI


[1] Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: FMOODS 1997: International Workshop on Formal Methods for Open Object-Based Distributed Systems, pp. 423–438. Chapman and Hall, Boca Raton (1997)
[2] Gardner, W.B.: Bridging CSP and C++ with Selective Formalism and Executable Specifications. In: MEMOCODE 2003: International Conference on Formal Methods and Models for Co-Design, pp. 237–245. IEEE Computer Society, Los Alamitos (2003)
[3] Goldsmith, M., Roscoe, B., Armstrong, P.: Failures-Divergence Refinement - FDR2 User Manual (2005), http://www.fsel.com/fdr2_manual.html
[4] Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International, Englewood Cliffs (1985) · Zbl 0637.68007
[5] Isobe, Y., Roggenbach, M.: A Generic Theorem Prover of CSP Refinement. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 108–123. Springer, Heidelberg (2005) · Zbl 1087.68592
[6] Kleine, M., Sanders, J.W.: Simulating truly concurrent CSP. Technical Report 434, UNU-IIST, P.O. Box 3058, Macau (June 2010) · Zbl 1325.68160
[7] Kwiatkowska, M., Phillips, I.: Possible and Guaranteed Concurrency in CSP. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 220–235. Springer, Heidelberg (1995)
[8] Leuschel, M., Fontaine, M.: Probing the Depths of CSP-M: A new FDR-compliant Validation Tool. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 278–297. Springer, Heidelberg (2008) · Zbl 05362221
[9] Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (2005)
[10] Scattergood, B.: The Semantics and Implementation of Machine-readable CSP. PhD thesis, University of Oxford (1998)
[11] Sun, J., Liu, Y., Dong, J.S.: Model Checking CSP Revisited: Introducing a Process Analysis Toolkit. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 307–322. Springer, Heidelberg (2008)
[12] Taubner, D., Vogler, W.: Step failures semantics and a complete proof system. Acta Inf. 27(2), 125–156 (1989) · Zbl 0689.68105
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.