MODEL CHECKING OF COMPONENT BASED SOFTWARE USING COMPOSITIONAL REDUCTIONS

2008 ◽  
Vol 18 (05) ◽  
pp. 683-712 ◽  
Author(s):  
MOHAMMAD IZADI ◽  
ALI MOVAGHAR
Keyword(s):  
Model Checking ◽  
Composition Operators ◽  
Linear Time ◽  
Operational Semantics ◽  
Computing System ◽  
Transition System ◽  
Compositional Model ◽  
Temporal Properties ◽  
Labeled Transition System ◽  
Constraint Automata

A component-based computing system consists of two main parts: a set of components and a coordination subsystem. Reo is an exogenous coordination language for compositional construction of the coordination subsystem. Constraint automaton has been defined as the operational semantics of Reo. The main goal of this paper is to prepare a model checking method for verifying linear time temporal properties of component-based systems whose coordinating subsystems are modeled by Reo and components are modeled by labeled transition systems. For this purpose, we introduce modified definitions of constraint automata and their composition operators by which, every constraint automaton can be considered as a labeled transition system and each labeled transition system can be translated into a constraint automaton. We show that failure-based equivalences CFFD and NDFD are congruences with respect to the composition operators of constraint automata. Also we present a method for compositional model checking of component-based systems using these equivalences for reducing the sizes of constraint automata models.

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

2021 ◽  
Author(s):  
Maxime Cordy ◽  
Sami Lazreg ◽  
Mike Papadakis ◽  
Axel Legay
Keyword(s):  
Model Checking ◽  
Statistical Model ◽  
Linear Time ◽  
The State ◽  
Coarse Grained ◽  
Bug Detection ◽  
Statistical Model Checking ◽  
Fine Grained ◽  
Type 1 Error ◽  
First Case

AbstractWe 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.

Two Approaches to Bounded Model Checking for Linear Time Logic with Knowledge

2012 ◽  
pp. 514-523 ◽  
Author(s):  
Artur Męski ◽  
Wojciech Penczek ◽  
Maciej Szreter ◽  
Bożena Woźna-Szcześniak ◽  
Andrzej Zbrzezny
Keyword(s):  
Model Checking ◽  
Linear Time ◽  
Bounded Model Checking ◽  
Time Logic

Logical foundations of hierarchical model checking

2018 ◽  
Vol 52 (4) ◽  
pp. 539-563 ◽  
Author(s):  
Norihiro Kamide
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Hierarchical Model ◽  
Design Methodology ◽  
Linear Time ◽  
Hierarchical Systems ◽  
Content Type ◽  
Computation Tree Logic ◽  
Computation Tree ◽  
Linear Time Temporal Logic

Purpose The purpose of this paper is to develop new simple logics and translations for hierarchical model checking. Hierarchical model checking is a model-checking paradigm that can appropriately verify systems with hierarchical information and structures. Design/methodology/approach In this study, logics and translations for hierarchical model checking are developed based on linear-time temporal logic (LTL), computation-tree logic (CTL) and full computation-tree logic (CTL*). A sequential linear-time temporal logic (sLTL), a sequential computation-tree logic (sCTL), and a sequential full computation-tree logic (sCTL*), which can suitably represent hierarchical information and structures, are developed by extending LTL, CTL and CTL*, respectively. Translations from sLTL, sCTL and sCTL* into LTL, CTL and CTL*, respectively, are defined, and theorems for embedding sLTL, sCTL and sCTL* into LTL, CTL and CTL*, respectively, are proved using these translations. Findings These embedding theorems allow us to reuse the standard LTL-, CTL-, and CTL*-based model-checking algorithms to verify hierarchical systems that are modeled and specified by sLTL, sCTL and sCTL*. Originality/value The new logics sLTL, sCTL and sCTL* and their translations are developed, and some illustrative examples of hierarchical model checking are presented based on these logics and translations.

Sign in / Sign up

Export Citation Format

Share Document