Mathematica in Formal Methods
- Development of a package to use VDM-SL structures in Mathematica
- 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).