FuseIC3

An Algorithm for Checking Large Design Spaces

Rohit Dureja and Kristin Yvonne Rozier

This webpage contains further details and artifacts for reproducibility of the experiments in "FuseIC3: An Algorithm for Checking Large Design Spaces" by R. Dureja and K.Y. Rozier.

---

1. NASA's NextGen Air Traffic Control System Models (ATC)

In the early phases of design, there is a need for the ability to analyze different design solutions. The family of NASA’s NextGen air traffic control (ATC) system models are a portfolio of potential design solutions to be compared with respect to different functional allocations, and overall reliability of the system. The entire design space consists of more than 20,000 designs. Each of the design is modeled as a labeled transition system and checked against a set of properties. The designs differ in terms of the parameters configured (different functional allocations).

Of the more than 20,000 designs, the relevant 1,620 are analyzed exhaustively. Each of the 1620 instances is checked against a total of 54 LTL properties, of which 34 are safety properties, and the rest are liveness. In our evaluation we consider safety properties only. The set is modeled in the SMV language, and uses OCRA for compositional modeling. The parameters to the system are specified using preprocessor directives. Each parameter configuration generates an unique model in the set. More details on the benchmark can be found on the project website.

2. Selected Benchmarks from HWMCC 2015

We evaluate FuseIC3 against a total of 548 benchmark models from the single safety property track of the Hardware Model Checking Competition 2015. To create a model-set from each benchmarks, we generated 200 mutations of each. The original model was mutated to only modify the transition system, and not the safety property implicit in the AIGER file; 1% of the assignments were randomly modified. An assignment of the form g = g1 ∧ g2 was selected with probability 0.01 and changed to g = 0, g = 1, g = ¬g1 ∧ g2, g = g1 ∧ ¬g2, g = ¬g1 ∧ ¬g2, g = g1 ∧ g2, g = g1, g = ¬g1, g = g2, or g = ¬g2, with equal probability.

3. Boeing's AIR 6110 Wheel Braking System Models (WBS)

The Aerospace Information Report (AIR) is a document issued by SAE. It provides an example application of recommended processes (ARP4754A and ARP4761) to a specific aircrat function. The example of a wheel brake system (WBS) demonstrates the applicability of design and safety techniques. The WBS consists of a complex hydraulic plant controller by a computer with varying operating modes, and two landing gears each with four wheels. The AIR 6110 guides the reader through a manual process leading to the development of several architecture variants satisfying both functional and safety requirements.

In the case study, seven architectures of the WBS are exhaustively checked. The architectures are modeled compositionally using OCRA, and xSAP is used for safety analysis. For our analysis, we derive the seven SMV models from the compositional architecture. Each model is checked against approxmiately 300 safety properties (these properties were contracts in original design methodology used). More details on the benchmark can be found on the project website.