Simultaneous SAT-Based Model Checking of Safety Properties

2006 ◽  
pp. 56-75 ◽  
Author(s):  
Zurab Khasidashvili ◽  
Alexander Nadel ◽  
Amit Palti ◽  
Ziyad Hanna
Keyword(s):  
Model Checking ◽  
Safety Properties

VERIFICATION OF EMBEDDED SUPERVISORY CONTROLLERS CONSIDERING HYBRID PLANT DYNAMICS

2005 ◽  
Vol 15 (02) ◽  
pp. 307-312 ◽  
Author(s):  
SEBASTIAN ENGELL ◽  
SVEN LOHMANN ◽  
OLAF STURSBERG
Keyword(s):  
Model Checking ◽  
Embedded Systems ◽  
Timed Automata ◽  
Processing System ◽  
Hybrid Plant ◽  
Graph Grammars ◽  
Safety Properties ◽  
Hybrid Automaton ◽  
Plant Behavior ◽  
Hybrid Dynamics

This contribution proposes a link between the specification of supervisory controllers by Sequential Function Charts (SFC) and the verification of embedded systems with hybrid dynamics. The SFC are transformed into modular timed automata using a procedure based on graph grammars. The resulting controller model is composed with a hybrid automaton (with possibly nonlinear continuous dynamics) that models the plant behavior. In order to verify safety properties of the composed system algorithmically, a tool implementing the recently proposed approach of counterexample guided model checking is employed. The procedure is illustrated for a processing system example.

scholarly journals Verification Method of Safety Properties of Embedded Assembly Program by Combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions

Electronics ◽  
2020 ◽  
Vol 9 (7) ◽  
pp. 1060
Author(s):  
Satoshi Yamane ◽  
Junpei Kobashi ◽  
Kosuke Uemura
Keyword(s):  
Model Checking ◽  
High Reliability ◽  
Bounded Model Checking ◽  
Point Of View ◽  
Satisfiability Modulo Theories ◽  
Prototype Model ◽  
Safety Properties ◽  
Verification Method ◽  
Interrupt Handler ◽  
Direct Operation

Embedded software has properties dependent on hardware (direct operation of address spaces, memory mapped I/O, interruption, etc.). Therefore, demands about the established method of formal verifications corresponding to those properties are increasing from the point of view of shorter development and high reliability. Our study aims at enabling a formal verification with Satisfiability Modulo Theories-Based Bounded Model Checking (SMT-Based BMC) of safety for embedded assembly codes. Our proposed method generates models of assembly codes in detail with the fixed-sized bit-vectors theory. The models generated by our method include interrupts, and the size of the models is reduced using Interrupt Handler Execution Reduction (IHER) technique. In this paper, we have developed the verification method of safety properties of embedded assembly program by combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions. Moreover, we show the evaluation of our method by experiments using prototype model checker.

scholarly journals Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)

2020 ◽  
pp. 378-382
Author(s):  
Hernán Ponce-de-León ◽  
Florian Furbach ◽  
Keijo Heljanko ◽  
Roland Meyer
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Memory Models ◽  
Memory Model ◽  
Complete Analysis ◽  
Concurrent Programs ◽  
Sequential Consistency ◽  
Model Checker ◽  
Safety Properties ◽  
C Programs

Abstract Dartagnanis a bounded model checker for concurrent programs under weak memory models. What makes it different from other tools is that the memory model is not hard-coded inside Dartagnanbut taken as part of the input. For SV-COMP’20, we take as input sequential consistency (i.e. the standard interleaving memory model) extended by support for atomic blocks. Our point is to demonstrate that a universal tool can be competitive and perform well in SV-COMP. Being a bounded model checker, Dartagnan’s focus is on disproving safety properties by finding counterexample executions. For programs with bounded loops, Dartagnanperforms an iterative unwinding that results in a complete analysis. The SV-COMP’20 version of Dartagnanworks on Boogiecode. The C programs of the competition are translated internally to Boogieusing SMACK.

Sign in / Sign up

Export Citation Format

Share Document