Modeling and Validating Hybrid Systems Using VDM and Mathematica

TL;DR

This paper presents a novel approach combining VDM and Mathematica to model, simulate, and validate hybrid systems with discrete and continuous dynamics, demonstrated through a space safety example.

Contribution

It introduces a new Mathematica package that emulates VDM-SL, enabling integration of differential equations into formal specifications for hybrid system modeling.

Findings

Successful modeling and simulation of hybrid systems using the combined approach

Enhanced validation with interactive GUI and data animation

Application to the SAFER space safety system example

Abstract

Hybrid systems are characterized by the hybrid evolution of their state: A part of the state changes discretely, the other part changes continuously over time. Typically, modern control applications belong to this class of systems, where a digital controller interacts with a physical environment. In this article we illustrate how a combination of the formal method VDM and the computer algebra system Mathematica can be used to model and simulate both aspects: the control logic and the physics involved. A new Mathematica package emulating VDM-SL has been developed that allows the integration of differential equation systems into formal specifications. The SAFER example from Kelly (1997) serves to demonstrate the new simulation capabilities Mathematica adds: After the thruster selection process, the astronaut's actual position and velocity is calculated by numerically solving Euler's and Newton's equations for rotation and translation. Furthermore, interactive validation is supported by a graphical user interface and data animation.