scholarly journals Formal verification of signature-monitoring mechanisms by model checking

2012 ◽  
Vol 9 (4) ◽  
pp. 1431-1451 ◽  
Author(s):  
Lanfang Tan ◽  
Qingping Tan ◽  
Jianjun Xu ◽  
Huiping Zhou
Keyword(s):  
Model Checking ◽  
State Transition ◽  
Fault Tolerant ◽  
Operational Semantics ◽  
Transient Faults ◽  
Model Checker ◽  
Symbolic Model ◽  
Input Program ◽  
State Transition System ◽  
Original Approach

In recent decades, reliability in the presence of transient faults has been a significant problem. To mitigate the effects of transient faults, fault-tolerant techniques are proposed. However, validating the effectiveness of fault-tolerant techniques is another problem. In this paper, we present an original approach to evaluate the effectiveness of signature-monitoring mechanisms. The approach is based on model-checking principles. First, the fault tolerant model is proposed using step-operational semantics. Second, the fault model is refined into a state transition system that is translated into the input program of the symbolic model checker NuSMV. Using NuSMV, two reprehensive signature-monitoring algorithms are verified. The approach avoids the state space explosion problem and the verification was completed with practical time. The verification results reveal some undetected errors, which have not been previously observed.

scholarly journals Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution)

2021 ◽  
pp. 428-432
Author(s):  
Hernán Ponce-de-León ◽  
Thomas Haas ◽  
Roland Meyer
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Model Checker ◽  
Compiler Optimizations ◽  
Sequential Programs ◽  
Input Program ◽  
Order Of Magnitude ◽  
Speed Up ◽  
First Time ◽  
Bitwise Operations

AbstractWe describe the new features of the bounded model checker Dartagnan for SV-COMP ’21. We participate, for the first time, in the ReachSafety category on the verification of sequential programs. In some of these verification tasks, bugs only show up after many loop iterations, which is a challenge for bounded model checking. We address the challenge by simplifying the structure of the input program while preserving its semantics. For simplification, we leverage common compiler optimizations, which we get for free by using LLVM. Yet, there is a price to pay. Compiler optimizations may introduce bitwise operations, which require bit-precise reasoning. We evaluated an SMT encoding based on the theory of integers + bit conversions against one based on the theory of bit-vectors and found that the latter yields better performance. Compared to the unoptimized version of Dartagnan, the combination of compiler optimizations and bit-vectors yields a speed-up of an order of magnitude on average.

scholarly journals Bounded Model Checking of ETL Cooperating with Finite and Looping Automata Connectives

2013 ◽  
Vol 2013 ◽  
pp. 1-12 ◽  
Author(s):  
Rui Wang ◽  
Wanwei Liu ◽  
Tun Li ◽  
Xiaoguang Mao ◽  
Ji Wang
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Bounded Model Checking ◽  
Symbolic Model Checking ◽  
Model Checker ◽  
Symbolic Model ◽  
Complementary Technique

As a complementary technique of the BDD-based approach, bounded model checking (BMC) has been successfully applied to LTL symbolic model checking. However, the expressiveness of LTL is rather limited, and some important properties cannot be captured by such logic. In this paper, we present a semantic BMC encoding approach to deal with the mixture ofETLfandETLl. Since such kind of temporal logic involves both finite and looping automata as connectives, all regular properties can be succinctly specified with it. The presented algorithm is integrated into the model checker ENuSMV, and the approach is evaluated via conducting a series of imperial experiments.

scholarly journals Pono: A Flexible and Extensible SMT-Based Model Checker

2021 ◽  
pp. 461-474
Author(s):  
Makai Mann ◽  
Ahmed Irfan ◽  
Florian Lonsing ◽  
Yahan Yang ◽  
Hongce Zhang ◽  
...  
Keyword(s):  
Model Checking ◽  
Open Source ◽  
Research Direction ◽  
Ease Of Use ◽  
Symbolic Model Checking ◽  
Model Checker ◽  
Symbolic Model ◽  
And Performance ◽  
System Designs ◽  
Important Research Direction

AbstractSymbolic model checking is an important tool for finding bugs (or proving the absence of bugs) in modern system designs. Because of this, improving the ease of use, scalability, and performance of model checking tools and algorithms continues to be an important research direction. In service of this goal, we present , an open-source SMT-based model checker. is designed to be both a research platform for developing and improving model checking algorithms, as well as a performance-competitive tool that can be used for academic and industry verification applications. In addition to performance, prioritizes transparency (developed as an open-source project on GitHub), flexibility ( can be adapted to a variety of tasks by exploiting its general SMT-based interface), and extensibility (it is easy to add new algorithms and new back-end solvers). In this paper, we describe the design of the tool with a focus on the flexible and extensible architecture, cover its current capabilities, and demonstrate that is competitive with state-of-the-art tools.

scholarly journals Verification and Strategy Synthesis for Coalition Announcement Logic

2021 ◽  
Author(s):  
Natasha Alechina ◽  
Hans van Ditmarsch ◽  
Rustam Galimullin ◽  
Tuo Wang
Keyword(s):  
Model Checking ◽  
Proof Of Concept ◽  
Model Checker ◽  
Complete Model ◽  
Concept Model ◽  
The Family ◽  
Winning Strategies ◽  
Epistemic Goals

AbstractCoalition announcement logic (CAL) is one of the family of the logics of quantified announcements. It allows us to reason about what a coalition of agents can achieve by making announcements in the setting where the anti-coalition may have an announcement of their own to preclude the former from reaching its epistemic goals. In this paper, we describe a PSPACE-complete model checking algorithm for CAL that produces winning strategies for coalitions. The algorithm is implemented in a proof-of-concept model checker.

Sign in / Sign up

Export Citation Format

Share Document