Abstract
Event-B is a refinement-based formal method that is used for system-level modeling and analysis of concurrent and distributed systems. Work has been done to extend Event-B with discrete time constraints. However the previous work does not capture the communication and competition between concurrent processes. In this paper, we distinguish task-based timing properties with scheduler-based timing properties from the perspective of different system design phases. To refine task-based timing properties with scheduler-based timing properties based on existing trigger-response patterns, we introduce a nondeterministic queue based scheduling framework to schedule processes under concurrent circumstances, which addresses the problems of refining deadline constraint under concurrent situations. Additional gluing invariants are provided to this refinement. To demonstrate the usability of the framework, we provide approaches to refine this framework with FIFO scheduling policy as well as deferrable priority based scheduling policy with aging technique. We demonstrate our framework and refinement with a timed mutual exclusion case study. The model is proved using the Rodin tool.
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 subscriptionsReferences
Abrial, J.R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)
Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)
Alur, R., Henzinger, T.A.: Finitary fairness. In: Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 52–61, July 1994
Alur, R.: Principles of Cyber-Physical Systems. The MIT Press, Cambridge (2015)
Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)
Banach, R., Butler, M., Qin, S., Verma, N., Zhu, H.: Core hybrid Event-B I: single hybrid Event-B machines. Sci. Comput. Program. 105, 92–123 (2015)
Butler, M.: Mastering System Analysis and Design through Abstraction and Refinement. IOS Press, Amsterdam (2013). http://eprints.soton.ac.uk/349769/
Butler, M., Abrial, J.R., Banach, R.: Modelling and refining hybrid systems in Event-B and Rodin. In: Petre, L., Sekerinski, E. (eds.) From Action System to Distributed Systems: The Refinement Approach. Taylor & Francis, April 2016. https://eprints.soton.ac.uk/376053/
Butler, M., Falampin, J.: An approach to modelling and refining timing properties in B, January 2002. https://eprints.soton.ac.uk/256235/
Cansell, D., Méry, D., Rehm, J.: Time constraint patterns for Event B development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 140–154. Springer, Heidelberg (2006). https://doi.org/10.1007/11955757_13
Dershowitz, N., Jayasimha, D.N., Park, S.: Bounded fairness. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 304–317. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-39910-0_14
Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 114–129. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75454-1_10
Graf, S., Prinz, A.: Time in state machines. Fundam. Inform. 77, 143–174 (2007)
Jastram, M., Butler, P.: Rodin User’s Handbook: Covers Rodin V.2.8. 2.8covers Rodin. Createspace Independent Pub, North Charleston (2014). https://books.google.co.uk/books?id=ws2WoAEACAAJ
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1–2), 134–152 (1997)
Sarshogh, M.R., Butler, M.: Specification and refinement of discrete timing properties in Event-B. In: AVoCS 2011 (2011). https://eprints.soton.ac.uk/272480/
Sekerinski, E., Zhang, T.: Finitary fairness in Event-B. In: Dagstuhl Seminar on Refinement Based Methods for the Construction of Dependable Systems. Dagstuhl, Germany (2009)
Sekerinski, E., Zhang, T.: Finitary fairness in action systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 319–336. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39718-9_19
Sulskus, G., Poppleton, M., Rezazadeh, A.: An interval-based approach to modelling time in Event-B. In: Dastani, M., Sirjani, M. (eds.) FSEN 2015. LNCS, vol. 9392, pp. 292–307. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24644-4_20. http://eprints.soton.ac.uk/377201/
Acknowledgement
This work is supported in part by the scholarship from China Scholarship Council (CSC) under the Grant CSC NO. 201708060147.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Zhu, C., Butler, M., Cirstea, C. (2018). Refinement of Timing Constraints for Concurrent Tasks with Scheduling. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science(), vol 10817. Springer, Cham. https://doi.org/10.1007/978-3-319-91271-4_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-91271-4_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-91270-7
Online ISBN: 978-3-319-91271-4
eBook Packages: Computer ScienceComputer Science (R0)