More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D3)

Rohit Dureja and Kristin Yvonne Rozier

This webpage contains details and artifacts for reproducibility of the experiments in "More Scalable LTL Model Checking via Discovering Design-Space Dependencies" by R. Dureja and K.Y. Rozier.

NASA's NextGen Air Traffic Control System Models

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. The model checking problem is split in to five phases;

  • Phase I: Airspace validation
  • Phase II: Nominal validation
  • Phase III: Extended validation
  • Phase IV: Nominal verification
  • Phase V: Extended verification

The nominal and extended models differ in terms of the faults modeled with the latter containing several possible faults. The airspace model captures the system without separation assurance agents (only contain aircraft). Each of the 1,620 models can be seen as instances of a combinatorial transition system with 7 enumerated parameters. Each of the 1620 instances is checked against a total of 346 properties, of which 191 are LTL properties, and the rest are CTL. The combinatorial transition system is modeled in the SMV language, uses OCRA for compositional modeling. The parameters to the system are specified using preprocessor directives.

More details on the benchmark can be found on the project website.

Boeing AIR 6110 Wheel Braking System Models

AIR 6110 employs informal methods to examine several WBS architectures which meet the same requirements with different degrees of reliability. In the published case study,

  • AIR 6110 is analyzed with formal methods.
  • WBS architectures in Air6110 are created in a formal manner.
  • The several architectures are automatically analyzed and compared.

From the perspective of a benchmark, these are a set of seven real-world nuXmv models representing possible designs for the Boeing AIR 6110 wheel braking system. Each model in set is checked against approximately 200 LTL properties. We evaluate D3 against this benchmark to measure its performance in multi-property verification workflows.

More details on the benchmark can be found on the project website.