More Scalable LTL Model Checking via Discovering Design-Space Dependencies (\(D^{3}\))

In the early phases of design, there are frequently many different models of the system under development [2, 23, 29] constituting a design space. We may need to evaluate different design choices, to check core capabilities of system versions with varying feature-levels, or to analyze a future version against previous ones in the product line. The models may differ in their assumptions, implementations, and configurations. We can use model checking to aid system development via a thorough comparison of the set of system models against a set of properties representing requirements. Model checking, in combination with related techniques like fault-tree analysis, can provide an effective comparative analysis [23, 29]. The classical approach checks each model one-by-one, as a set of independent model-checking runs. For large and complex design spaces, performance can be inefficient or even fail to scale to handle the combinatorial size of the design space. Nevertheless, the classical approach remains the most widely used method in industry [3, 23, 25, 29, 30]. Algorithms for family-based model checking [11, 13] mitigate this problem but their efficiency and applicability still depends on the use of custom model checkers to deal with model families.

We assume that each model in the design space can be parameterized over a finite set of parametric inputs that enable/disable individual assumptions, implementations, or behaviors. It might be the case that for any pair of models the assumptions are dependent, their implementations contradict each other, or they have the same behavior. Since the different models of the same system are related, it is possible to exploit the known relationships between them, if they exist, to optimize the model checking search. These relationships can exist in two ways: relationships between the models, and relationships between the properties checked for each model.

We present an algorithm that automatically prunes and dynamically orders the model-checking search space by exploiting inter-model relationships. The algorithm, Discover Design-Space Dependencies (\(D^{3}\)), 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, \(D^{3}\) works with any off-the-shelf checker. This allows practitioners to use state-of-the-art, optimized model-checking algorithms, and to choose their preferred model checker, which enables adoption of our method by practitioners who already use model checking with minimum change in their verification workflow. 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. \(D^{3}\) 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 [33] to determine the dependencies between pairs of LTL properties, then reduces the number of properties that are checked for each instance. \(D^{3}\) 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. We demonstrate the industrial scalability of \(D^{3}\) using a set of 1,620 real-life, publicly-available SMV-language benchmark models with LTL specifications; these model NASA’s NextGen air traffic control system [8, 23, 29]. We also evaluate the property-dependence analysis separately on real-life models of Boeing AIR 6110 Wheel Braking System [3] to evaluate \(D^{3}\) in multi-property verification workflows.

Related Work. One striking contrast between \(D^{3}\) and related work is that \(D^{3}\) is a preprocessing algorithm, does not require custom modeling, and works with any off-the-shelf LTL model checker. Parameter synthesis [9] can generate the many models in a design space that can be analyzed by \(D^{3}\); however existing parameter synthesis techniques require custom modeling of a system. We take the easier path of reasoning over an already-restricted set of models of interest to system designers. \(D^{3}\) efficiently compares any set of models rather than finding all models that meet the requirements. Several parameter synthesis approaches designed for parametric Markov models [15, 16, 24, 31] use PRISM and compute the region of parameters for which the model satisfies a given probabilistic property (PCTL or PLTL); \(D^{3}\) is an LTL-based algorithm. Parameter synthesis of a parametric Markov model with non-probabilistic transitions can generate the many models that \(D^{3}\) can analyze. In multi-objective model checking [1, 21, 22, 28], given a Markov decision process and a set of LTL properties, the algorithms find a controller strategy such that the Markov process satisfies all properties with some set probability. Differently from multi-objective model checking, which generates “trade-off” Pareto curves, \(D^{3}\) gives a boolean result. The parameterized model checking problem (PCMP) [20] deals with infinite families of homogeneous processes in a system; in our case, the models are finite and heterogeneous. Specialized model-set checking algorithms [18] can check the reduced set of \(D^{3}\) processed models.

In multi-property model checking, multiple properties are checked on the same system. Existing approaches simplify the task by algorithm modifications [4, 7], SAT-solver modifications [26, 27], and property grouping [5, 6]. The inter-property dependence analysis of \(D^{3}\) can be used in multi-property checking. We compare \(D^{3}\) against the affinity [6] based approach to property grouping.

Product line verification techniques, e.g., with Software Product Lines (SPL), also verify parametric models describing large design spaces. We borrow the notion of an instance, from SPL literature [32, 34]. An extension to NuSMV in [13] performs symbolic model checking of feature-oriented CTL. The symbolic analysis is extended to the explicit case and support for feature-oriented LTL in [11, 12]. The work most closely related to ours is [17] where product line verification is done without a family-based model checker. \(D^{3}\) outputs model-checking results for every model-property pair in the design space (e.g. all parameter configurations) without dependence on any feature whereas in SPL verification using an off-the-shelf checker, if a property fails then it isn’t possible to know which models do satisfy the property [14, 17].

Contributions. The preprocessing algorithm presented is an important stepping stone to smarter algorithms for checking large design spaces. Our contributions are summarized as follows:

A computation path, or run of LTS M is a sequence of states \(\pi = s_0 {\rightarrow } s_1 {\rightarrow } \ldots {\rightarrow } s_n\) over the word \(w = L(s_0), L(s_1), \ldots , L(s_n)\) such that \(s_i \in S\) for \(0 \le i \le n\), and \((s_i, s_{i+1}) \in \delta \) for \(0 \le i < n\). Given a LTL property \(\varphi \) and a LTS M, M models \(\varphi \), denoted \(M \models \varphi \), iff \(\varphi \) holds in all possible computation paths of M.

Let P be a finite set of parameters. |P| denotes the number of parameters. For each \(P_i \in P\), \(|P_i|\) denotes the size of the domain of \(P_i\). Let Form(P) denote the set of all Boolean formulas over P generated using the BNF grammar \({\varphi }\, {:}{:=}~\top \mid P_i {\text { { == }}} \text {D} \) and \( \text {D}\, {:}{:=}~P_{i_1} \mid P_{i_2} \mid \ldots \mid P_{i_n};\) for each \(P_i \in P\), \(n = |P_i|\), and \(\llbracket P_i \rrbracket ~{=}~\{P_{i_1}, P_{i_2}, \ldots , P_{i_n}\}\). Therefore, Form(P) contains \(\top \) and equality constraints over parameters in P.

We limit the guard condition over a transition to \(\top \) or an equality constraint over a single parameter for simpler expressiveness and formalization. However, there can be multiple transitions between any two states with different guards. A transition is enabled if its guard condition evaluates to true, otherwise, it is disabled. A label of \(\top \) implies the transition is always enabled. A possible run of a CTS is a sequence of states \(\pi _P = s_0 {\mathrel {\mathop {\rightarrow }\limits ^{\nu _1}}} s_1 {\mathrel {\mathop {\rightarrow }\limits ^{\nu _2}}} \ldots {\mathrel {\mathop {\rightarrow }\limits ^{\nu _n}}} s_n\) over the word \(w = L(s_0), L(s_1), \ldots , L(s_n)\) such that \(s_i \in S\) for \(0 \le i \le n\), \(\nu _i \in Form(P)\) for \(0 < i \le n\), and \((s_i, s_{i+1}) \in \delta \) and \((s_i, s_{i+1}, \nu _{i+1}) \in L_P\) for \(0 \le i < n\), i.e., there is transition from \(s_i\) to \(s_{i+1}\) with guard condition \(\nu _{i+1}\). A prefix \(\alpha \) of a possible run \(\pi _P = \alpha {\mathrel {\mathop {\rightarrow }\limits ^{\nu _i}}} \ldots {\mathrel {\mathop {\rightarrow }\limits ^{\nu _n}}}s_n\) is also a possible run.

Example 1. A Boolean parameter has domain \(\{true,\) \(false\}\). Figure 1 shows a CTS with Boolean parameters \(P = \{P_1, P_2, P_3\}\). For brevity, guard condition \(P_i == true\) is written as \(P_i\), while \(P_i == false\) is written as \(\lnot P_i\). A transition with label \(P_1\) is enabled if \(P_1\) is set to true. Similarly, a label of \(\lnot P_3\) implies the transition is enabled if \(P_3\) is set to false.

A configured run of a CTS \(M_P\) over a configuration c, or c-run, is a sequence of states \(\pi _{P(c)} = s_0 \xrightarrow {\nu _1} s_1 \xrightarrow {\nu _2} \ldots \xrightarrow {\nu _n} s_n\) such that \(\pi _{P(c)}\) is a possible run, and \(c \vdash \nu _i\) for \(0 < i \le n\), where \(\vdash \) denotes propositional logic satisfaction of the guard condition \(\nu _i\) under parameter configuration c. Given a CTS \(M_P\) and a parameter configuration c, a state t is reachable iff there exists a c-run such that \(s_n = t\), denoted \(s_0 \xrightarrow [c]{*} t\), i.e., t can be reached in zero or more transitions. A transition with guard \(\nu \) is reachable iff \((s_j, s_{j+1}, \nu ) \in L_P\), \((s_j, s_{j+1}) \in \delta \), and \(s_0 \xrightarrow [c]{*} s_j\).

Given a LTL property \(\varphi \) and a CTS \(M_P = (\Sigma , S, s_0, L, \delta , P, L_P)\), the model checking problem for \(M_P\) is to find all parameter configurations \(c \in \mathbb {C}\) over P such that \(\varphi \) holds in all c-runs of \(M_P\), or all computation paths of LTS \(M_{P(c)}\).

Example 2 In Fig. 1, if \(P_1\) is set to false, execution never reaches the transition labeled \(\lnot P_3\). Therefore, if configuration \(c = (false, true, true)\) then \(P_3 \leadsto _c P_1\).

This theorem reduces LTL satisfiability checking to LTL model checking. Therefore, \(\varphi \) is satisfiable when the model checker finds a counterexample.¹

Modeling a Combinatorial Transition System. Efficient modeling of a CTS requires language constructs to deal with parameters. Since our goal is to use an existing model checker, language extensions are outside the scope of this work. An alternative way to add parameters to any system description is by utilizing the C preprocessor (cpp). Given a set of parameters P, and a combinatorial model \(M_P\), each run of the preprocessor with a configuration \(c \in \mathbb {C}\) generates an instance \(M_{P(c)}\). Figure 2 demonstrates generating a CTS from two related SMV models. Model 1 and Model 2 differ in the initial configuration of the parameter. The corresponding CTS replaces the parameter initiation with the PARAMETER_CONF preprocessor directive. The cpp is run on the CTS model with #define PARAMETER_CONF 0, and #define PARAMETER_CONF 1 to generate the two models.

In this section we describe \(D^{3}\). Our approach speeds up model checking of combinatorial transitions systems by preprocessing of the input instances; it therefore increases efficiency of both BDD-based and SAT-based model checkers. The problem reduction is along two dimensions: number of instances, and number of properties.

Our revised model checking procedure \(D^{3}\) is shown in Fig. 6. \(D^{3}\) takes as input a CTS \(M_P\) and a set of LTL properties \(\mathcal {P}\). It uses GenPC to find the parameter configurations that need to be checked. It then generates a property table to store dependencies between LTL properties. Lastly, CheckRP checks each instance against properties in \(\mathcal {P}\). Results are collated for every model-property pair.

We present an algorithm, \(D^{3}\), to increase the efficiency of LTL model checking for large design spaces. It is successful in reducing the number of models that need to be verified, and also the properties verified for each model. In contrast to software product line model checking techniques using an off-the-shelf checker, \(D^{3}\) returns the model-checking results for all models, and for all properties. \(D^{3}\) is general and extensible; it can be combined with optimized checking algorithms implemented in off-the-shelf model checkers. We demonstrate the practical scalability of \(D^{3}\) on a real-life benchmark models. We calculate a crossover point as a crucial measure of when \(D^{3}\) can be used to speed up checking. \(D^{3}\) is fully automated and requires no special input-language modifications; it can easily be introduced in a verification work-flow with minimal effort. Heuristics for predicting the cross-over point for other model sets are a promising topic for future work. We plan to examine extending \(D^{3}\) to other logics besides LTL, and its applicability to other types of transition systems, like families of Markov processes. We also plan to investigate further reduction in the search space by extending \(D^{3}\) to re-use intermediate model checking results across several models. In a nutshell, \(D^{3}\) is a front-end preprocessing algorithm, and future work involves tying in an improved model checking back-end and utilizing available information to reduce the overall amortized performance. Finally, since checking families of models is becoming commonplace, we plan to develop more industrial-sized SMV model sets and make them publicly available as research benchmarks.

The artifact for reproducibility of our experiments [19] is publicly available under the MIT License, and supports all reported results of Sect. 4. It includes

The artifact supports the following usage scenarios.

Please refer to the README files in the artifact for further information. Every README inside a directory details the directory structure, usage of contained files with respect to the evaluation, and step-by-step instructions on how to the use the contained scripts to regenerate the experimental analysis.