A Tool-Supported Approach for Modeling and Verifying Hybrid Systems using EVENT-B and the Differential Equation Solver SAGEMATH

: The common mathematical model for cyber-physical systems is that of hybrid systems that enable combining both discrete and continuous behaviors represented by differential equations. In this paper, we introduce a formal approach, using E VENT -B and its refinement strategy, for specifying and verifying cyber-physical systems whose behavior is described by ordinary differential equations. To deal with the resolution of ordinary differential equations in Event-B, the approach is based on interfacing the differential equation solver S AGE M ATH (System for Algebra and Geometry Experimentation) with the R ODIN tool, a platform for E VENT -B projects development. For this purpose, we modeled and implemented the interface to the solver in E VENT -B using a R ODIN plugin. This enables to reason on the E VENT -B specification and prove safety properties. The proposed approach was successfully applied on a frequently used cyber-physical system case studies.

• Publication year

  2023

• Venue

  International Conference on Software and Data Technologies

• Publication date

  Unknown publication date

• Fields of study

  Computer Science, Engineering

• Identifiers
  DOI 10.5220/0012080900003538
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Event-B Refinement for Continuous Behaviours Approximation

  2021cited by this paper
• Modelling Hybrid Programs with Event-B

  2020cited by this paper
• Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B

  2018cited by this paper
• Modelling and Refining Hybrid Systems in Event-B and Rodin

  2016cited by this paper
• Differential Refinement Logic*

  2016cited by this paper
• Core Hybrid Event-B I: Single Hybrid Event-B machines

  2015cited by this paper
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems

  2015cited by this paper
• Formalizing hybrid systems with Event-B and the Rodin Platform

  2014cited by this paper
• SpaceEx: Scalable Verification of Hybrid Systems

  2011cited by this paper
• Modeling in event-b - system and software engineering by Jean-Raymond Abrial

  2010cited by this paper
• Mathematical Extension in Event-B through the Rodin Theory Component

  2010cited by this paper
• Differential Dynamic Logic for Hybrid Systems

  2008cited by this paper
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)

  2008cited by this paper

• No citing papers are available for this paper.