×

zbMATH — the first resource for mathematics

A formal framework for Hybrid Event B. (English) Zbl 1351.68166
Xue, Jinyun (ed.) et al., Proceedings of the 6th international workshop on harnessing theories for tool support in software (TTSS 2013), Nanchang, China, October 27, 2013. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 309, 3-12, electronic only (2014).
Summary: In this paper, we present Hybrid Event B, a formal language for modeling hybrid systems. Specifically, Hybrid Event B is an extension of Event B associating with differential dynamic logic. The main contribution of this paper is that we give the definition of a differential event in Hybrid Event B, which makes it possible using differential dynamic logic in modeling continuous dynamical systems and discrete dynamical systems. In addition, we show the proof obligations of each refinements on differential events, which supports the stepwise development of refinement. We also show the transformer semantics of the differential events and the weakest precondition refinement approach applied to hybrid systems, both of which support our stepwise development of hybrid systems.
For the entire collection see [Zbl 1310.68021].
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68Q45 Formal languages and automata
68Q55 Semantics in the theory of computing
Software:
Rodin; Z
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur, R.; Courcoubetis, C.; Halbwachs, N.; Henzinger, T. A.; Ho, P. H.; Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., The algorithmic analysis of hybrid systems, Theor. Comput. Sci., 138, 1, 3-34, (1995) · Zbl 0874.68206
[2] Davoren, J. M.; Nerode, A., Logics for hybrid systems, IEEE, 88, 7, 985-1010, (July 2000)
[3] Henzinger, T. A., The theory of hybrid automata, (LICS, (1996), IEEE Computer Society Los Alamitos), 278-292
[4] Abrial, J.-R., Modeling in event-B: system and software engineering, (2010), Cambridge University Press · Zbl 1213.68214
[5] Platzer, A., Differential dynamic logic for hybrid systems, J. Autom. Reas., 41, 2, 143C189, (2008)
[6] Metayer, C.; Abrial, J.-R.; Voisin, L., (2005), accessed 25/5/10. bf
[7] Butler, M. J.; Hallerstede, S., The rodin formal modeling tool, (BCS-FACS Christmas 2007 Meeting Formal Methods In Industry, (2007))
[8] Abrial, J.-R.; Butler, M. J.; Hallerstede, S.; Voisin, L., A road map for the rodin toolset, (Borger, E.; Butler, M. J.; Bowen, J. P.; Boca, P., ABZ, Lecture Notes in Computer Science, vol. 5238, (2008), Springer), 347
[9] Abrial, J.-R.; Butler, M. J.; Hallerstede, S.; Hoang, T. S.; Mehta, F.; Voisin, L., Rodin: an open toolset for modelling and reasoning in event-B, STTT, 12, 6, 447-466, (2010)
[10] Woodcock, J. C.P.; Davies, J., Using Z: specification, refinement, and proof, (1996), Prentice Hall · Zbl 0855.68060
[11] Jackson, D., Alloy: a lightweight object modelling notation, ACM Trans. Softw. Eng. Methodol., 11, 2, 256-290, (2002)
[12] Platzer, A., Differential-algebraic dynamic logic for differential-algebraic programs, J. Log. Comput., 20, 1, 309-352, (2010) · Zbl 1191.03024
[13] Platzer, A., Logical analysis of hybrid systems: proving theorems for complex dynamics, (2010), Springer Heidelberg · Zbl 1211.68412
[14] Platzer, A., The complete proof theory of hybrid systems, (Nov 2011), School of Computer Science, Carnegie Mellon University Pittsburgh, PA, Tech. Rep. CMU-CS-11-144
[15] Back, R. J.R., Refinement calculus, part II: parallel and reactive programs, (de Bakker, J. W.; de Roever, W.-P.; Rozenberg, G., Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness. Proceedings, 1989, Lecture Notes in Computer Science, vol. 430, (1990), Springer-Verlag)
[16] Ronkko, M.; Sere, K., Refinement and continuous behavior, (Vaandrager, F. W.; van Schuppen, J. H., Proceedings of Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, vol. 1569, (1999), Springer Berlin), 223-237 · Zbl 0930.68030
[17] Platzer, A.; Clarke, E. M., The image computation problem in hybrid systems model checking, (Bemporad, A.; Bicchi, A.; Buttazzo, G., HSCC, LNCS, vol. 4416, (2007), Springer Berlin), 473-486 · Zbl 1221.93118
[18] Henzinger, T. A., The theory of hybrid automata, (LICS, (1996), IEEE Computer Society Los Alamitos), 278-292
[19] Zhou, C.; Ravn, A. P.; Hansen, M. R., An extended duration calculus for hybrid real-time systems, (Grossman, R. L.; Nerode, A.; Ravn, A. P.; Rischel, H., Hybrid Systems, LNCS, vol. 736, (1992), Springer Berlin), 36-59
[20] Jifeng, H., From CSP to hybrid systems, (Roscoe, A. W., A Classical Mind: Essays in Honour of C. A. R. Hoare, (1994), Prentice Hall Hertfordshire), 171-189
[21] Chaochen, Z.; Ji, W.; Ravn, A. P., Aformal description of hybrid systems, (Alur, R.; Henzinger, T. A.; Sontag, E. D., Hybrid Systems, LNCS, vol. 1066, (1995), Springer Berlin), 511-530
[22] Davoren, J. M.; Nerode, A., Logics for hybrid systems, Proc. IEEE, 88, 7, 985-1010, (2000)
[23] Davoren, J. M., On hybrid systems and the modal-calculus, (Antsaklis, P. J.; Kohn, W.; Lemmon, M. D.; Nerode, A.; Sastry, S., Hybrid Systems, LNCS, vol. 1567, (1997), Springer Berlin), 38-69 · Zbl 0928.93027
[24] Ronkkon, M.; Ravn, A. P.; Sere, K., Hybrid action systems, Theor. Comput. Sci., 290, 1, 937-973, (2003) · Zbl 1019.68054
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.