基于VDM和Mathematica的混合系统建模与验证
Modeling and Validating Hybrid Systems Using VDM and Mathematica
摘要：
混杂系统的特征在于其状态的混杂演化：一部分状态离散地变化，另一部分状态随时间连续地变化。通常，现代控制应用属于这类系统，其中数字控制器与物理环境交互。在这篇文章中，我们说明了如何结合的形式化方法VDM和计算机代数系统Mathematica可以用来建模和模拟两个方面：控制逻辑和物理参与。一个新的Mathematica软件包仿真VDM-SL已经开发，允许微分方程系统集成到正式规范。来自Kelly（1997）的SAFER示例用于演示新的仿真功能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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
