Author(s)

J. Gunnarsson & R. Germundsson

Abstract

Tools for Verification of a Large Discrete Sys- tem J. Gunnarsson & R. Germundsson Department of Electrical Engineering, Linkoping University, S-581 83 Linkoping, Sweden Email: johan@isy.liu.se Abstract 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. 1 Introduction 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

Keywords