Author(s): J. Gunnarsson & R. Germundsson
Tools for modeling and verification of discrete event systems are imple-
mented 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.
We have modeled and analyzed an existing discrete subsystem of a modern
fighter aircraft, the landing gear system on the JAS 39 Gripen, depicted in
Size: 555 kb
Paper DOI: 10.2495/IMS970271
the Full Article
This article is part of the WIT OpenView scheme and you can download the full text Adobe PDF article for FREE by clicking the 'Openview' icon below.
this page to a colleague.