Abstract
CSP treats internal τ 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 τs, it has sometimes been necessary to be careful about the interpretation of τ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 τ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.
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
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)
Armstrong, P., Lowe, G., Ouaknine, J., Roscoe, A.W.: Model checking Timed CSP. To appear in Proceedings of HOWARD, Easychair
Hopcroft, P.J., Broadfoot, G.H.: Combining the box structure development method and CSP. Electr. Notes Theor. Comput. Sci. 128(6), 127–144 (2005)
Broadfoot, G.H., Hopcroft, P.J.: A paradigm shift in software development. In: Proceedings of Embedded World Conference 2012, Nuremberg, February 29 (2012)
Fidge, C.J.: A formal definition of priority in CSP. ACM Transactions on Programming Languages and Systems 15(4) (1993)
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)
Hoare, C.A.R.: Communicating sequential processes. Prentice Hall (1985)
Lawrence, A.E.: CSPP and event priority. Communicating Process Architectures 59 (2001)
Lowe, G.: Probabilistic and prioritised models of Timed CSP. Theoretical Computer Science 138(2) (1995)
Phillips, I.: Refusal testing. Theoretical Computer Science 50(3) (1987)
Roscoe, A.W.: Model checking CSP. In: A Classical Mind: Essays in Honour of C.A.R. Hoare. Prentice Hall (1994)
Roscoe, A.W.: The theory and practice of concurrency. Prentice Hall (1997)
Roscoe, A.W.: Understanding concurrent systems. Springer (2010)
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)
Schneider, S.A.: Concurrent and real-time systems: the CSP approach. Wiley (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Roscoe, A.W., Hopcroft, P.J. (2013). Slow Abstraction via Priority. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theories of Programming and Formal Methods. Lecture Notes in Computer Science, vol 8051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39698-4_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-39698-4_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39697-7
Online ISBN: 978-3-642-39698-4
eBook Packages: Computer ScienceComputer Science (R0)