Tools for Verification of a Large Discrete System
1997 (English)In: Innovation in Mathematics, 1997, 199-206 p.Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
1997. 199-206 p.
Modeling, Verification, Binary decision diagrams, Boolean expressions, Fighter aircraft, Pascal
IdentifiersURN: urn:nbn:se:liu:diva-93797ISBN: 9781853125058OAI: oai:DiVA.org:liu-93797DiVA: diva2:626801
Proceedings of the Second International Mathematica Symposium, Rovaniemi, Finland, June-July, 1997