Wolfram Library Archive

Courseware Demos MathSource Technical Notes
All Collections Articles Books Conference Proceedings

Modeling and validating hybrid systems using VDM and Mathematica

B. K. Aichernig
Reinhold Kainhofer
Journal / Anthology

LFM 2000: Fifth NASA Langley Formal Methods Workshop (NASA/CP-2000-210100). NASA. Hampton, VA, USA. -- Proceedings of 5th NASA Langley Formal Methods Workshop. Williamsburg, VA, USA. 13-15 June 2000
Year: 2000
Page range: 35-46

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. 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 and Kemp, 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.

*Engineering > Control Theory