Wolfram Library Archive

Courseware Demos MathSource Technical Notes
All Collections Articles Books Conference Proceedings

Tools for verification of a large discrete system

Johan Gunnarsson
Organization: MathCore Engineering AB
URL: http://www.mathcore.com
Roger Germundsson
Organization: Wolfram Research, Inc.
Department: Director of Research & Development
Journal / Anthology

Innovation in Mathematics: Proceedings of the Second International Mathematica Symposium
Year: 1997
Page range: 199-206

Tools for modeling and verification of discrete event systems are implemented in Mathematica. The tools are based on binary decision diagrams (BDD) for which a Mathematica interface is provided. For modeling a compiler is developed translating a restricted class of Pascal into boolean expressions represented by BDDs. The tools are used in an application of a landing gear system of a fighter aircraft. This system is controlled by a software consisting of 1200 lines of Pascal. This code represented as a BDD is then analyzed using temporal logics. This article demonstrates the principle of the Pascal compiler.

*Engineering > Aeronautical and Astronautical Engineering
*Engineering > Control Theory
*Mathematics > Foundations of Mathematics > Logic