Model Checking of Embedded Systems Using RTCTL While Generating Timed Kripke Structure

2018 ◽  
Author(s):  
Yajun Wu ◽  
Satoshi Yamane
Keyword(s):  
Model Checking ◽  
Embedded Systems ◽  
Kripke Structure

scholarly journals Compositional Verification using Model Checking and Theorem Proving

2020 ◽  
pp. 305-314
Author(s):  
Diego Marmsoler
Keyword(s):  
Distributed Systems ◽  
Model Checking ◽  
Embedded Systems ◽  
Theorem Proving ◽  
Formal Modeling ◽  
Compositional Verification ◽  
Modeling And Analysis ◽  
Simple Version ◽  
Evolving Systems ◽  
Alternative Approach

AbstractCollaborative embedded systems form groups in which individual systems collaborate to achieve an overall goal. To this end, new systems may join a group and participating systems can leave the group. Classical techniques for the formal modeling and analysis of distributed systems, however, are mainly based on a static notion of systems and thus are often not well suited for the modeling and analysis of collaborative embedded systems. In this chapter, we propose an alternative approach that allows for the verification of dynamically evolving systems and we demonstrate it in terms of a running example: a simple version of an adaptable and flexible factory.

Model Checking for SpaceWire Error Detection Module

2012 ◽  
Vol 241-244 ◽  
pp. 3020-3025
Author(s):  
Ling Ling Dong ◽  
Yong Guan ◽  
Xiao Juan Li ◽  
Zhi Ping Shi ◽  
Jie Zhang ◽  
...  
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Temporal Logic ◽  
Error Detection ◽  
System Model ◽  
Linear Search ◽  
Kripke Structure ◽  
Mathematical Methods ◽  
Safety Critical ◽  
Correctness Of Programs

Considerable attention has been devoted to prove the correctness of programs. Formal verification overcomes the incompleteness by applying mathematical methods to verify a design. SpaceWire is a well known communication standard. For safety-critical applications an approach is needed to validate the completeness of SpareWire design. This paper addresses formal verification of SpareWire error detection module. The system model was constructed by Kripke structure, and the properties were presented by linear temporal logic (LTL). Compared the verification of LTL with CTL (branch temporal logic), LTL properties could improve the verification efficiency due to its linear search. The error priority was checked using simulation guided by model checking. After some properties were modified, all possible behaviors of the module satisfied the specification. This method realizes complete validation of the error detection module.

scholarly journals Semantic Consistency Checking in Building Ontology from Heterogeneous Sources

2014 ◽  
Vol 2014 ◽  
pp. 1-11 ◽  
Author(s):  
Shihan Yang ◽  
Hongyan Tan ◽  
Jinzhao Wu
Keyword(s):  
Model Checking ◽  
Heterogeneous Data ◽  
Domain Ontology ◽  
Semistructured Data ◽  
Data Sources ◽  
Consistency Checking ◽  
Kripke Structure ◽  
Semantic Consistency ◽  
Heterogeneous Data Sources ◽  
Consistency Problem

Semantic collision is inevitable while building a domain ontology from heterogeneous data sources (semi-)automatically. Therefore, the semantic consistency is indispensable precondition for building a correct ontology. In this paper, a model-checking-based method is proposed to handle the semantic consistency problem with a kind of middle-model methodology, which could extract a domain ontology from structured and semistructured data sources semiautomatically. The method translates the middle model into the Kripke structure, and consistency assertions into CTL formulae, so a consistency checking problem is promoted to a global model checking. Moreover, the feasibility and correctness of the transformation is proved, and case studies are provided.

A new model for model checking: cycle-weighted Kripke structure

2010 ◽  
Vol 4 (1) ◽  
pp. 78-88
Author(s):  
Jiaqi Zhu ◽  
Hanpin Wang ◽  
Zhongyuan Xu ◽  
Chunxiang Xu
Keyword(s):  
Model Checking ◽  
Kripke Structure ◽  
New Model

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.

Sign in / Sign up

Export Citation Format

Share Document