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.
Abstract
Modern system design often requires comparing several models over a large design space. Different models arise out of a need to weigh different design choices, to check core capabilities of versions with varying features, or to analyze a future version against previous ones. Model checking can compare different models; however, applying model checking off-the-shelf may not scale due to the large size of the design space for today’s complex systems. We exploit relationships between different models of the same (or related) systems to optimize the model checking search. Our algorithm, D3, preprocesses the design space and checks fewer model-checking instances, e.g., using nuXmv. It automatically prunes the search space by reducing both the number of models to check, and the number of LTL properties that need to be checked for each model in order to provide the complete model-checking verdict for every individual model-property pair. We formalize heuristics that improve the performance of D3. We demonstrate the scalability of D3 by extensive experimental evaluation, e.g., by checking 1,620 real-life models for NASA’s NextGen air traffic control system. Compared to checking each model-property pair individually, D3 is up to 9.4× faster.
Algorithm
The algorithm, Discover Design-Space Dependencies (D3), reduces both the number of models to check, and the number of LTL properties that need to be checked for each model. Rather than using a custom model checker, D3 works with any off-the-shelf checker. We reason about a set of system models by introducing the notion of a Combinatorial Transition System (CTS). Each individual model, or instance, can be derived from the CTS by configuring it with a set of parameters. Each transition in the CTS is enabled/disabled by the parameters. We model check each instance of the CTS against sets of properties. We assume the properties are in Linear Temporal Logic (LTL) and are independent of the choice of parameters, though not all properties may apply to all instances. D3 preprocesses the CTS to find relationships between parameters and minimizes the number of instances that need to be checked to produce results for the whole set. It uses LTL satisfiability checking to determine the dependencies between pairs of LTL properties, then reduces the number of properties that are checked for each instance. D3 returns results for every model-property pair in the design space, aiming to compose these results from a reduced series of model-checking runs compared to the classical approach of checking every model-property pair.