Abstract
Following a brief discussion of uniprocessor scheduling in which we argue the case for formal analysis, we describe a distributed Event B model of interrupt driven scheduling. We first consider a model with two executing tasks, presented with the aid of state machine diagrams. We then present a faulty variant of this model which, under particular event timings, may ”drop” an interrupt. We show how the failure to discharge a particular proof obligation leads us to the conceptual error in this model. Finally we generalise the correct model to n tasks, leading to a reduction in proof effort.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R., Cansell, D.: Refinement and Reachability in Event B. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 222–241. Springer, Heidelberg (2005)
Butler, M.: csp2B: A practical approach to combining CSP and B. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, Springer, Heidelberg (1999)
Stoddart, W.J., Dunne, S.E., Galloway, A.J., Shore, R.: Abstract State Machines: Designing Distributed Systems with State Machines and B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, Springer, Heidelberg (1998)
Papatsaras, A., Stoddart, W.J.: Global and Communicating State Machine Models in Event Driven B: A Simple Railway Case Study. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, Springer, Heidelberg (2002)
Liu, C.L., Layland, J.W.: Scheduling algorithms for multiprogramming in a hard real-time environment. Journal of the ACM 20(1) (1973)
Klein, M., et al.: A Practitioners Handbook for Real time Analysis. Kluwer Academic Pub., Dordrecht (1993)
Reeves, G.: What really happened on Mars? Risks Forum Digest 19(58) (1998)
Abrial, J.-R.: The B Book. Cambridge University Press, Cambridge (1996)
Schneider, S., Treharne, H.: Communicating B Machines. In: Bert, D., P. Bowen, J., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, Springer, Heidelberg (2002)
Abrial, J.-R., Cansell, D.: Click’n’Prove: Interactive Proofs in Set Theory. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stoddart, B., Cansell, D., Zeyda, F. (2006). Modelling and Proof Analysis of Interrupt Driven Scheduling. In: Julliand, J., Kouchnarenko, O. (eds) B 2007: Formal Specification and Development in B. B 2007. Lecture Notes in Computer Science, vol 4355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11955757_14
Download citation
DOI: https://doi.org/10.1007/11955757_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68760-3
Online ISBN: 978-3-540-68761-0
eBook Packages: Computer ScienceComputer Science (R0)