Dupont, Guillaume and Aït-Ameur, Yamine
and Pantel, Marc
and Singh, Neeraj Kumar
Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B.
(2018)
In: International Conference Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2018), 5 June 2018 - 8 June 2018 (Southampton, United Kingdom).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 711kB |
Official URL: https://doi.org/10.1007/978-3-319-91271-4_11
Abstract
The design of hybrid systems controllers requires one to handle both discrete and continuous functionalities in a single development framework. In this paper, we propose the design and verification of such controllers using a correct-by-construction approach. We use proof-based formal methods to model and verify the required safety properties of the given controllers. Both Event-B with Rodin, and hybrid programs and dynamic differential logic with KeYmaera are experimented on a common case study related to the modelling of a car controller. Finally, we discuss the lessons learnt from these experiments and draw the first steps towards a generic method for modelling hybrid systems in Event-B.
Item Type: | Conference or Workshop Item (Paper) |
---|---|
Additional Information: | Thanks to Springer editor. This papers appears in volume 10817 of Lecture Notes in Computer Science ISSN : 0302-9743 ISBN: 978-3-319-91270-7 The original PDF is available at: https://link.springer.com/chapter/10.1007/978-3-319-91271-4_11 |
HAL Id: | hal-02450998 |
Audience (conference): | International conference proceedings |
Uncontrolled Keywords: | |
Institution: | Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE) French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE) Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE) Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE) Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE) |
Laboratory name: | |
Statistics: | download |
Deposited On: | 17 Jan 2020 09:54 |
Repository Staff Only: item control page