Symbolic tools for verification of large scale DEDS

Binary decision diagrams (BDDs) have been used to represent relations, as well as the operations for modeling, analysis and synthesis of DEDS. To utilize the structure of integers and arithmetic operation, integer decision diagrams (IDDs) are developed to represent integer structures and arithmetic operations efficiently. With tools for efficient relational representation, it possible to improve scalability of DEDS computations, as illustrated by the modeling and analysis of the landing gear controller of the Swedish fighter aircraft JAS 39 Gripen. A relational model, represented both by a BDD and an IDD, is automatically generated from a 1200 lines Pascal implementation, which contains 105 binary variables of which 26 are state variables. Function specifications expressed with temporal algebra are verified using tools for dynamic analysis, which we also use to compute a relation representing the set of all reachable states in the model. The landing gear controller serves as a benchmark test of BDDs and IDDs. The IDDs reduced the computation time by 50%.