Statistical model checking for variability-intensive systems: applications to bug detection and minimization

We propose a new Statistical Model Checking (SMC) method to identify bugs in variability-intensive systems (VIS). The state-space of such systems is exponential in the number of variants, which makes the verification problem harder than for classical systems. To reduce verification time, we propose to combine SMC with featured transition systems (FTS)—a model that represents jointly the state spaces of all variants. Our new methods allow the sampling of executions from one or more (potentially all) variants. We investigate their utility in two complementary use cases. The first case considers the problem of finding all variants that violate a given property expressed in Linear-Time Logic (LTL) within a given simulation budget. To achieve this, we perform random walks in the featured transition system seeking accepting lassos. We show that our method allows us to find bugs much faster (up to 16 times according to our experiments) than exhaustive methods. As any simulation-based approach, however, the risk of Type-1 error exists. We provide a lower bound and an upper bound for the number of simulations to perform to achieve the desired level of confidence. Our empirical study involving 59 properties over three case studies reveals that our method manages to discover all variants violating 41 of the properties. This indicates that SMC can act as a coarse-grained analysis method to quickly identify the set of buggy variants. The second case complements the first one. In case the coarse-grained analysis reveals that no variant can guarantee to satisfy an intended property in all their executions, one should identify the variant that minimizes the probability of violating this property. Thus, we propose a fine-grained SMC method that quickly identifies promising variants and accurately estimates their violation probability. We evaluate different selection strategies and reveal that a genetic algorithm combined with elitist selection yields the best results.

Verifying Stochastic Hybrid Systems with Temporal Logic Specifications via Model Reduction

We present a scalable methodology to verify stochastic hybrid systems for inequality linear temporal logic (iLTL) or inequality metric interval temporal logic (iMITL). Using the Mori–Zwanzig reduction method, we construct a finite-state Markov chain reduction of a given stochastic hybrid system and prove that this reduced Markov chain is approximately equivalent to the original system in a distributional sense. Approximate equivalence of the stochastic hybrid system and its Markov chain reduction means that analyzing the Markov chain with respect to a suitably strengthened property allows us to conclude whether the original stochastic hybrid system meets its temporal logic specifications. Based on this, we propose the first statistical model checking algorithms to verify stochastic hybrid systems against correctness properties, expressed in iLTL or iMITL. The scalability of the proposed algorithms is demonstrated by a case study.

Overview of Control Algorithm Verification Methods in Power Electronics Systems

The paper presents the existing verification methods for control algorithms in power electronics systems, including the application of model checking techniques. In the industry, the most frequently used verification methods are simulations and experiments; however, they have to be performed manually and do not give a 100% confidence that the system will operate correctly in all situations. Here we show the recent advancements in verification and performance assessment of power electronics systems with the usage of formal methods. Symbolic model checking can be used to achieve a guarantee that the system satisfies user-defined requirements, while statistical model checking combines simulation and statistical methods to gain statistically valid results that predict the behavior with high confidence. Both methods can be applied automatically before physical realization of the power electronics systems, so that any errors, incorrect assumptions or unforeseen situations are detected as early as possible. An additional functionality of verification with the use of formal methods is to check the converter operation in terms of reliability in various system operating conditions. It is possible to verify the distribution and uniformity of occurrence in time of the number of transistor switching, transistor conduction times for various current levels, etc. The information obtained in this way can be used to optimize control algorithms in terms of reliability in power electronics. The article provides an overview of various verification methods with an emphasis on statistical model checking. The basic functionalities of the methods, their construction, and their properties are indicated.