 |
|
|
|
|
 |
|
|
Tools for verification of a large discrete system
|
|
|
|
|
|
| Organization: | MathCore Engineering AB |
| Organization: | Wolfram Research, Inc. |
| Department: | Director of Research & Development |
|
|
|
|
|
|
| Innovation in Mathematics: Proceedings of the Second International Mathematica Symposium |
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
For the newest resources, visit Wolfram Repositories and Archives »
