Modeling and Validating Hybrid Systems Using VDM and Mathematica
<|reference_start|>Modeling and Validating Hybrid Systems Using VDM and Mathematica: 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.<|reference_end|>
@article{aichernig2004modeling,
    title={Modeling and Validating Hybrid Systems Using VDM and Mathematica},
    author={Bernhard K. Aichernig and Reinhold Kainhofer},
    journal={In C.Michael Holloway, editor, Lfm2000, Fifth NASA Langley Formal
  Methods Workshop, Williamsburg, Virginia, June 2000, number CP-2000-210100,
  pages 35-46. NASA, June 2000},
    year={2004},
    archivePrefix={arXiv},
    eprint={cs/0407050},
    primaryClass={cs.SE}
}