Abstract
The concept of interrupts is important in system specifications across both software and hardware. However, behaviours of interrupts are difficult to capture particularly in a timed environment because of its complexity. In this paper, the catastrophic interrupt adopted by the standard CSP models, the generic interrupt presented by Hoare in his original CSP book and the timed interrupt (time-driven) given in Timed CSP are considered in Circus Time. The contribution of the paper is a development of the reactive design semantics of these three interrupt operators in the UTP, a collection of verified laws, and a comprehensive discussion on the subtle difference between catastrophic and generic interrupts in applications.
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
Roscoe, A.W.: Model-checking CSP. In: A Classical Mind: essays in Honour of C.A.R. Hoare, ch. 21. Prentice-Hall (1994)
Cavalcanti, A.L.C., Woodcock, J.C.P.: A Tutorial Introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220–268. Springer, Heidelberg (2006)
Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A Refinement Strategy for Circus. Formal Aspects of Computing 15(2-3), 146–181 (2003)
Feliachi, A., Gaudel, M.-C., Wolff, B.: Isabelle/Circus : A Process Specification and Verification Environment. Technical Report 1547, LRI, Université Paris-Sud XI (November 2011), http://www.lri.fr/Rapports-internes
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall International (1985)
Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall International (1998)
Huang, Y., Zhao, Y., Shi, J., Zhu, H., Qin, S.: Investigating time properties of interrupt-driven programs. In: Gheyi, R., Naumann, D. (eds.) SBMF 2012. LNCS, vol. 7498, pp. 131–146. Springer, Heidelberg (2012)
Jifeng, H.: From CSP to hybrid systems, pp. 171–189 (1994)
Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
McEwan, A., Woodcock, J.C.P.: Unifying theories of interrupts. In: Proceedings of the Second UTP Symposium, Trinity College Dublin (2008)
Morgan, C.: Programming from specifications. Prentice-Hall, Inc., Upper Saddle River (1990)
Oliveira, M., Cavalcanti, A.L.C., Woodcock, J.C.P.: Unifying theories in ProofPower-Z. Formal Aspects of Computing Journal (2007)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall International (1998)
Schneider, S.A.: Concurrent and real-time systems: the CSP approach. John Wiley & Sons (1999)
Sherif, A., Cavalcanti, A.L.C., Jifeng, H., Sampaio, A.C.A.: A process algebraic framework for specification and validation of real-time systems. Formal Aspects of Computing 22(2), 153–191 (2010)
Wei, K., Woodcock, J.C.P., Burns, A.: A timed model of Circus with the reactive design miracle. In: 8th International Conference on Software Engineering and Formal Methods (SEFM), Pisa, Italy, pp. 315–319. IEEE Computer Society (September 2010)
Wei, K., Woodcock, J.C.P., Burns, A.: Timed Circus: Timed CSP with the Miracle. In: ICECCS, pp. 55–64 (2011)
Wei, K., Woodcock, J.C.P., Cavalcanti, A.L.C.: Circus Time with reactive designs. In: UTP, pp. 68–87 (2012)
Wei, K., Woodcock, J.C.P., Cavalcanti, A.L.C.: New Circus Time. Technical report, Department of Computer Science, University of York, UK (March 2012), http://www.cs.york.ac.uk/circus/hijac/publication.html
Woodcock, J.C.P., Davies, J.: Using Z: Specification, Refinement and Proof. Prentice-Hall, Inc., Upper Saddle River (1996)
Woodcock, J.C.P., Cavalcanti, A.L.C.: A concurrent language for refinement. In: Butterfield, A., Pahl, C. (eds.) IWFM 2001: 5th Irish Workshop in Formal Methods, BCS Electronic Workshops in Computing, Dublin, Ireland (July 2001)
Woodcock, J.C.P., Cavalcanti, A.L.C.: The Semantics of $ Circus$. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)
Woodcock, J.C.P., Cavalcanti, A.L.C.: A Tutorial Introduction to Designs in Unifying Theories of Programming. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 40–66. Springer, Heidelberg (2004)
Zhao, Y., Huang, Y., He, J., Liu, S.: Formal Model of Interrupt Program from a Probabilistic Perspective. In: ICECCS, pp. 87–94 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wei, K. (2013). Reactive Designs of Interrupts in Circus Time . In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theoretical Aspects of Computing – ICTAC 2013. ICTAC 2013. Lecture Notes in Computer Science, vol 8049. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39718-9_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-39718-9_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39717-2
Online ISBN: 978-3-642-39718-9
eBook Packages: Computer ScienceComputer Science (R0)