×

zbMATH — the first resource for mathematics

Translating between models of concurrency. (English) Zbl 07203615
The main idea of this study is to harness a model checker for coarser semantics to model check finer semantics, using an operator with respect to which the coarser semantics is not compositional. In the experiments in this study, the coarser semantics is trace semantics and the operator is priority. The finer semantics may be any known semantics between stable acceptances and traces, and it is conjectured that it may also be any “reasonable” unknown semantics in this range. The stable acceptance semantics records finite sequences consisting of alternating precise (as opposed to minimal) stable acceptance sets / non-observation markers and visible actions. The study covers the whole range from abstract theory to medium-scale concrete experiments. The writing is CSP-specific, but at least the general ideas are formalism-independent. The last third of the study extends the ideas to timed CSP, yielding the first practical automated compositional method that uses the FDR tool. Where points of comparison were available, the new approach proved somewhat but not horribly less efficient than the earlier ones. The authors speculate that with bigger alphabets, the results may become worse. However, the goal is not to beat custom implementations but to provide something useful in their absence.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q55 Semantics in the theory of computing
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
FDR3; Uppaal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Armstrong, P., Lowe, G., Ouaknine, J., Roscoe, A.W.: Model checking Timed CSP. In: Proceedings of HOWARD (Festschrift for Howard Barringer) (2012)
[2] Brinksma, E., Rensink, A., Vogler, W.: Fair testing. In: International Conference on Concurrency Theory, pp. 313-327. Springer, Berlin (1995)
[3] Davies, J.; Schneider, S., A brief history of Timed CSP, Theor. Comput. Sci., 138, 2, 243-271 (1995) · Zbl 0874.68162
[4] Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3—a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2014. Lecture Notes in Computer Science, vol. 8413, Springer, Berlin, Heidelberg (2014) · Zbl 1392.68300
[5] Gibson-Robinson, T.; Armstrong, P.; Boulgakov, A.; Roscoe, AW, FDR3: a parallel refinement checker for CSP, Int. J. Softw. Tools Technol. Transf., 18, 2, 149-167 (2016)
[6] Gibson-Robinson, T., Hansen, H., Roscoe, A.W., Wang, X.: Practical partial order reduction for CSP. In: Havelund K., Joshi R., Holzmann G. (eds.) NASA Formal Methods, pp. 188-203. Springer, Berlin (2015)
[7] Hoare, CAR, Communicating Sequential Processes (1985), Upper Saddle River: Prentice-Hall Inc, Upper Saddle River · Zbl 0637.68007
[8] Jackson, D.M.: Logical verification of reactive software systems. Oxford University, DPhil Thesis (1992)
[9] Kanellakis, PC; Smolka, SA, CCS expressions, finite state processes, and three problems of equivalence, Inf. Comput., 86, 1, 43-68 (1990) · Zbl 0705.68063
[10] Larsen, KG; Pettersson, P.; Yi, W., UPPAAL in a nutshell, Int. J. Softw. Tools Technol. Transf. (STTT), 1, 1, 134-152 (1997) · Zbl 1060.68577
[11] Mestel, D.; Roscoe, AW, Reducing complex CSP models to traces via priority, Electron. Notes Theor. Comput. Sci., 325, 237-252 (2016) · Zbl 1392.68310
[12] Milner, R., A Calculus of Communicating Systems (1982), New York: Springer, New York
[13] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, I, Inf. Comput., 100, 1, 1-40 (1992) · Zbl 0752.68036
[14] Ouaknine, J.: Discrete analysis of continuous behaviour in real-time concurrent systems. PhD thesis, Oxford University (2000)
[15] Ouaknine, J.: Digitisation and full abstraction for dense-time model checking. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 37-51. Springer, Berlin (2002) · Zbl 1043.68581
[16] Phillips, I., Refusal testing, Theor. Comput. Sci., 50, 3, 241-284 (1987) · Zbl 0626.68011
[17] Reed, GM; Roscoe, AW, The timed failures-stability model for CSP, Theor. Comput. Sci., 211, 1-2, 85-127 (1999) · Zbl 0912.68038
[18] Roscoe, AW, The Theory and Practice of Concurrency (1997), Upper Saddle River: Prentice Hall PTR, Upper Saddle River
[19] Roscoe, A.W.: Seeing beyond divergence. In: Communicating Sequential Processes. The First 25 Years, pp. 15-35. Springer, Berlin (2005) · Zbl 1081.68062
[20] Roscoe, AW, Revivals, stuckness and the hierarchy of CSP models, J. Logic Algebr. Program., 78, 3, 163-190 (2009) · Zbl 1171.68025
[21] Roscoe, AW, Understanding Concurrent Systems (2010), Berlin: Springer, Berlin · Zbl 1211.68205
[22] Roscoe, A.W.: On the expressiveness of CSP (2011)
[23] Roscoe, A.W.: The automated verification of timewise refinement. EIT- CPSE (2013)
[24] Roscoe, AW, The expressiveness of CSP with priority, Electron. Notes Theor. Comput. Sci., 319, 387-401 (2015) · Zbl 1351.68148
[25] Roscoe, AW; Dathi, N., The pursuit of deadlock freedom, Inf. Comput., 75, 3, 289-327 (1987) · Zbl 0626.68019
[26] Roscoe, AW; Huang, J., Checking noninterference in Timed CSP, Form. Asp. Comput., 25, 1, 3-35 (2013) · Zbl 1259.68132
[27] Roscoe, AW; Reed, GM, A timed model for Communicating Sequential Processes, Theor. Comput. Sci., 58, 249-261 (1988) · Zbl 0655.68031
[28] Schneider, S., An operational semantics for Timed CSP, Inf. Comput., 116, 2, 193-213 (1995) · Zbl 0827.68069
[29] Schneider, S., Concurrent and Real-Time Systems (2000), Hoboken: Wiley, Hoboken
[30] Shallit, J., A Second Course in Formal Languages and Automata Theory (2009), Cambridge: Cambridge University Press, Cambridge · Zbl 1163.68025
[31] van Glabbeek, R.J.: The linear time-branching time spectrum II. In: International Conference on Concurrency Theory, pp. 66-81 (1993)
[32] Van Glabbeek, R.J.: The linear time-branching time spectrum I. The semantics of concrete, sequential processes. In: Handbook of Process Algebra, pp. 3-99. Elsevier, Amsterdam (2001) · Zbl 1035.68073
[33] www.cs.ox.ac.uk/people/publications/personal/Bill.Roscoe.html (paper 193)
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.