Reinhold Kainhofer

Mathematica in Formal Methods

1. Development of a package to use VDM-SL structures in Mathematica
2. Including the physical model in hybrid systems in formal methods

Software project / Seminar paper in Softwaretechnology

With this project in Software Technology I try to remedy a big disadvantage in formal methods: Most tools don't support any or only very few mathematical functions. So when you work with PVS, the VDM-SL toolbox or Z, you cannot include the physical model which is mostly described as a set of differential equations.

For the project, I wrote a package for Mathematica that implements the VDM-SL (Vienna Development Method - Specification language) in Mathematica, so that from now on the discrete control model can be combined with the physical model described by mathematical functions. As an example, I implemented NASA's SAFER (Simplified aid for extravehicular rescue) backbag.

• View the Lfm2000 paper (pdf, 234kB)
• Download the whole package (source code and documentation as notebooks, 226 kB)
• Download the HTML version of the seminar work (327 kB)

We (B. Aichernig and I) submitted a paper about this package for the NASA Formal Methods Workshop 2000 (LFM2000, Full proceedings).