×

Slow abstraction via priority. (English) Zbl 1390.68487

Liu, Zhiming (ed.) et al., Theories of programming and formal methods. Essays dedicated to Jifeng He on the occasion of his 70th birthday. Berlin: Springer (ISBN 978-3-642-39697-7/pbk). Lecture Notes in Computer Science 8051, 326-345 (2013).
Summary: CSP treats internal \(\tau \) actions as urgent, so that an infinite sequence of them is the misbehaviour known as divergence, and states with them available make no offer that we can rely on. While it has been possible to formulate a number of forms of abstraction in these models where the abstracted actions become \(\tau \)s, it has sometimes been necessary to be careful about the interpretation of \(\tau \)s and divergence. In this paper, inspired by an industrial problem, we demonstrate how this range of abstractions can be extended to encompass the offers made by processes during a run of “slow \(\tau \)s”, namely abstractions of interactions with an external agent that does not usually respond urgently to an offer, but always eventually does respond. This extension requires the prioritise operator recently introduced into CSP and its refinement checker FDR. We demonstrate its use in the modelling used in Verum’s ASD:Suite.
For the entire collection see [Zbl 1269.68023].

MSC:

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

Software:

ASD Suite
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Armstrong, P., Goldsmith, M., Lowe, G., Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: Recent developments in FDR. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 699–704. Springer, Heidelberg (2012) · Zbl 06070780 · doi:10.1007/978-3-642-31424-7_52
[2] Armstrong, P., Lowe, G., Ouaknine, J., Roscoe, A.W.: Model checking Timed CSP. To appear in Proceedings of HOWARD, Easychair
[3] Hopcroft, P.J., Broadfoot, G.H.: Combining the box structure development method and CSP. Electr. Notes Theor. Comput. Sci. 128(6), 127–144 (2005) · Zbl 1272.68111 · doi:10.1016/j.entcs.2005.04.008
[4] Broadfoot, G.H., Hopcroft, P.J.: A paradigm shift in software development. In: Proceedings of Embedded World Conference 2012, Nuremberg, February 29 (2012)
[5] Fidge, C.J.: A formal definition of priority in CSP. ACM Transactions on Programming Languages and Systems 15(4) (1993) · doi:10.1145/155183.155221
[6] Goldsmith, M., Moffat, N., Roscoe, A., Whitworth, T., Zakiuddin, I.: Watchdog transformations for property-oriented model-checking. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 600–616. Springer, Heidelberg (2003) · doi:10.1007/978-3-540-45236-2_33
[7] Hoare, C.A.R.: Communicating sequential processes. Prentice Hall (1985) · Zbl 0637.68007
[8] Lawrence, A.E.: CSPP and event priority. Communicating Process Architectures 59 (2001)
[9] Lowe, G.: Probabilistic and prioritised models of Timed CSP. Theoretical Computer Science 138(2) (1995) · Zbl 0874.68163 · doi:10.1016/0304-3975(94)00171-E
[10] Phillips, I.: Refusal testing. Theoretical Computer Science 50(3) (1987) · Zbl 0626.68011 · doi:10.1016/0304-3975(87)90117-4
[11] Roscoe, A.W.: Model checking CSP. In: A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice Hall (1994)
[12] Roscoe, A.W.: The theory and practice of concurrency. Prentice Hall (1997)
[13] Roscoe, A.W.: Understanding concurrent systems. Springer (2010) · Zbl 1211.68205 · doi:10.1007/978-1-84882-258-0
[14] Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M.H., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133–152. Springer, Heidelberg (1995) · doi:10.1007/3-540-60630-0_7
[15] Schneider, S.A.: Concurrent and real-time systems: the CSP approach. Wiley (2000)
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.