Speaker: Dominique Méry
Abstract: Hybrid systems are widely used in a variety of safety-critical applications. Therefore, it is vital to provide a high-level safety guarantee for their implementations. Based on the action system and the refinement methodology, researchers show how to model a safe time-triggered design in the Event-B language. It consists of system events that monitor the system state periodically and make appropriate actuation decisions for the system’s safety. However, two crucial types of system events are missing in such design, i.e. sensing and actuation, which hinders the development of robust hybrid systems. In addition, Event-B is specialized in high-level system modeling. Its primitives are not expressive enough to naturally support refining system events into low-level software implementations.
In this work, we propose a way to refine (by decomposition) the time-triggered design to introduce the missing system events, without complex high-level system modeling. Based on the decomposition, we identify which system events are implementable. Then, we define a translational approach to the B language. Our translational approach: 1) systematically modularizes a specified Event-B software operation from associated system events. 2) defines a verified translation to obtain a semantically equivalent correspondent in the B language for each modularized Event-B software operation. This translational approach allows us to reuse the primitives of B for refining system events down to implementations, and reuse the predicate transformers defined on the B primitives to reason for the correctness of refinements. It also ensures that the behaviors of the implementations obtained via refinements in B do not divert from the corresponding system events specified in Event-B.
Bio: Dominique Méry (http://members.loria.fr/Mery and http://mery54.github.io/Mery) has been Full Professor of Computing Science at University of Lorraine since September 1993, Head of the Research Group (Formal Methods and Applications) at LORIA, and Head of the PhD School IAEM Lorraine. His professional skills include acting as Expert for NSF, Enterprise Ireland, ANR, AERES HCERES. His academic titles are PhD in Computer Science and Thèse d’état (1993, Mathematics/Computing Science). His Prizes and Professional Achievements include Member of l’Institut Universitaire de France (1995-2000), Grant for Scientific Excellence, Member of IFIP WG 1.3 (Foundations of System Specification). Member of the editorial board of Formal Aspects of Computing (ACM) and Science of Computer Programming (Elsevier). He has been pc chairs of several conferences as FM, ICFEM, TASE, ICTAC, ICCESS, iFM and pc members of iFM, FM, TASE, ICTAC etc.
Topics of research focus on proof-oriented system development for computer-based systems and aim at ensuring higher levels of reliability and correctness. Recent and current researches have addressed the incremental proof-based development of distributed algorithms and the proof-based modelling of medical devices as pacemaker as well as cyber-physical systems. Main objectives are to address the use of refinement in the modelling process and links with certification questions.