Formal Methods for Verifications of Reactive Systems

2011 ◽  
pp. 376-415
Author(s):  
Olfa Mosbahi ◽  
Mohamed Khalgui
Keyword(s):  
Theorem Proving ◽  
Reactive Systems ◽  
Prototype System ◽  
Model Checker ◽  
B Method ◽  
Liveness Properties ◽  
Finite State ◽  
Infinite State Systems ◽  
Sorting System ◽  
Event B Method

This chapter deals with the use of two verification approaches: theorem proving and model checking. The authors focus on the Event-B method by using its associated theorem proving tool (Click_n_Prove), and on the language TLA+ by using its model checker TLC. By considering the limitation of the Event-B method to invariance properties, the authors propose to apply the language TLA+ to verify liveness properties on a software behavior. The authors extend first the expressivity and the semantics of a B model (called temporal B model) to deal with the specification of fairness and eventuality properties. Second, they give transformation rules from a temporal B model into a TLA+ module. The authors present in particular, their prototype system called B2TLA+, that they have developed to support this transformation; then they can verify these properties thanks to the model checker TLC on finite state systems. For the verification of infinite-state systems, they propose the use of the predicate diagrams. The authors illustrate their approach on a case study of a parcel sorting system.

scholarly journals Automatic verification of timed concurrent constraint programs

2006 ◽  
Vol 6 (3) ◽  
pp. 265-300 ◽  
Author(s):  
MORENO FALASCHI ◽  
ALICIA VILLANUEVA
Keyword(s):  
Model Checking ◽  
Infinite Number ◽  
Reactive Systems ◽  
Finite Model ◽  
Computation Model ◽  
Huge Number ◽  
Finite State ◽  
Infinite State Systems ◽  
Infinite State ◽  
Concurrent Constraint Programming

The language Timed Concurrent Constraint (tccp) is the extension over time of the Concurrent Constraint Programming (cc) paradigm that allows us to specify concurrent systems where timing is critical, for example reactive systems. Systems which may have an infinite number of states can be specified in tccp. Model checking is a technique which is able to verify finite-state systems with a huge number of states in an automatic way. In the last years several studies have investigated how to extend model checking techniques to systems with an infinite number of states. In this paper we propose an approach which exploits the computation model of tccp. Constraint based computations allow us to define a methodology for applying a model checking algorithm to (a class of) infinite-state systems. We extend the classical algorithm of model checking for LTL to a specific logic defined for the verification of tccp and to the tccp Structure which we define in this work for modeling the program behavior. We define a restriction on the time in order to get a finite model and then we develop some illustrative examples. To the best of our knowledge this is the first approach that defines a model checking methodology for tccp.

Event-B method and liveness properties

2010 ◽  
Vol 44 (9-10) ◽  
pp. 1119-1163
Author(s):  
Olfa Mosbahi ◽  
Jacques Jaray
Keyword(s):  
B Method ◽  
Liveness Properties ◽  
Event B Method

USING COMPUTATION TREE LOGIC FOR INTELLIGENT INFORMATION SEARCH ON THE WEB

2002 ◽  
Vol 02 (03) ◽  
pp. 245-253 ◽  
Author(s):  
EUGENIO DI SCIASCIO ◽  
FRANCESCO M. DONINI ◽  
MARINA MONGIELLO
Keyword(s):  
Information Search ◽  
State Transition ◽  
Transition System ◽  
Prototype System ◽  
Retrieval Models ◽  
Computation Tree Logic ◽  
Computation Tree ◽  
Finite State ◽  
State Transition System ◽  
Intelligent Information

Web engines crawl hyperlinks to search for new documents; yet when they index discovered documents they basically revert to conventional information retrieval models and concentrate on the indexing of terms in a single document. We propose to overcome such limits with an approach based on temporal logic. By modeling a web site as a finite state transition system we are able to define complex and selective queries over hyperlinks with the aid of Computation Tree Logic operators. We deployed the proposed approach in a prototype system that allows users pose queries in natural language. Queries are automatically translated in Computation Tree Logic, and the answer returned by our system is a set of paths. Experiments carried out with the aid of human experts show improved retrieval effectiveness with respect to current search engines.

scholarly journals Mixed-semantics composition of statecharts for the component-based design of reactive systems

2020 ◽  
Vol 19 (6) ◽  
pp. 1483-1517
Author(s):  
Bence Graics ◽  
Vince Molnár ◽  
András Vörös ◽  
István Majzik ◽  
Dániel Varró
Keyword(s):  
Code Generation ◽  
Composite System ◽  
Formal Semantics ◽  
Reactive Systems ◽  
Cyber Physical System ◽  
Test Case ◽  
Model Checker ◽  
Model Driven Engineering ◽  
Design Decisions ◽  
Model Driven

Abstract The increasing complexity of reactive systems can be mitigated with the use of components and composition languages in model-driven engineering. Designing composition languages is a challenge itself as both practical applicability (support for different composition approaches in various application domains), and precise formal semantics (support for verification and code generation) have to be taken into account. In our Gamma Statechart Composition Framework, we designed and implemented a composition language for the synchronous, cascade synchronous and asynchronous composition of statechart-based reactive components. We formalized the semantics of this composition language that provides the basis for generating composition-related Java source code as well as mapping the composite system to a back-end model checker for formal verification and model-based test case generation. In this paper, we present the composition language with its formal semantics, putting special emphasis on design decisions related to the language and their effects on verifiability and applicability. Furthermore, we demonstrate the design and verification functionality of the composition framework by presenting case studies from the cyber-physical system domain.

SMT-based verification of data-aware processes: a model-theoretic approach

2020 ◽  
Vol 30 (3) ◽  
pp. 271-313
Author(s):  
Diego Calvanese ◽  
Silvio Ghilardi ◽  
Alessandro Gianola ◽  
Marco Montali ◽  
Andrey Rivkin
Keyword(s):  
Model Theory ◽  
Satisfiability Modulo Theories ◽  
Theoretic Approach ◽  
Model Checker ◽  
Present Contribution ◽  
Relational Systems ◽  
Infinite State Systems ◽  
Algorithmic Techniques ◽  
The One ◽  
Infinite State

AbstractIn recent times, satisfiability modulo theories (SMT) techniques gained increasing attention and obtained remarkable success in model-checking infinite-state systems. Still, we believe that whenever more expressivity is needed in order to specify the systems to be verified, more and more support is needed from mathematical logic and model theory. This is the case of the applications considered in this paper: we study verification over a general model of relational, data-aware processes, to assess (parameterized) safety properties irrespectively of the initial database (DB) instance. Toward this goal, we take inspiration from array-based systems and tackle safety algorithmically via backward reachability. To enable the adoption of this technique in our rich setting, we make use of the model-theoretic machinery of model completion, which surprisingly turns out to be an effective tool for verification of relational systems and represents the main original contribution of this paper. In this way, we pursue a twofold purpose. On the one hand, we isolate three notable classes for which backward reachability terminates, in turn witnessing decidability. Two of such classes relate our approach to conditions singled out in the literature, whereas the third one is genuinely novel. On the other hand, we are able to exploit SMT technology in implementations, building on the well-known MCMT (Model Checker Modulo Theories) model checker for array-based systems and extending it to make all our foundational results fully operational. All in all, the present contribution is deeply rooted in the long-standing tradition of the application of model theory in computer science. In particular, this paper applies these ideas in an original mathematical context and shows how these techniques can be used for the first time to empower algorithmic techniques for the verification of infinite-state systems based on arrays, so as to make such techniques applicable to the timely, challenging settings of data-aware processes.

Statechart-based Controllers Synthesis in FPGA Structures with Embedded Array Blocks

2010 ◽  
Vol 56 (1) ◽  
pp. 13-24 ◽  
Author(s):  
Grzegorz Łabiak ◽  
Grzegorz Borowik
Keyword(s):  
Complex Systems ◽  
Finite State Machine ◽  
Reactive Systems ◽  
State Machine ◽  
Embedded Memory ◽  
Digital Controllers ◽  
Functional Decomposition ◽  
Finite State ◽  
Implementation Scheme ◽  
Programmable Devices

Statechart-based Controllers Synthesis in FPGA Structures with Embedded Array BlocksStatechart diagrams, in general, are visual formalism for description of complex systems behaiour. Digital controllers, which act as reactive systems, can be very conveniently modeled with statecharts and efficiently synthesized in modern programmable devices. The paper presents in details syntax and semantics of statecharts and new implementation scheme. The issue of statecharts synthesis is not still ultimately solved. Main feature of the presented approach is the transformation of statechart diagrams into Finite State Machine, and through KISS format, functional decomposition and mapping into Embedded Memory Blocks. Embedded Memory are part of the modern programmable devices.

scholarly journals Identification of ICS Security Risks toward the Analysis of Packet Interaction Characteristics Using State Sequence Matching Based on SF-FSM

2017 ◽  
Vol 2017 ◽  
pp. 1-17 ◽  
Author(s):  
Jianxin Xu ◽  
Dongqin Feng
Keyword(s):  
Anomaly Detection ◽  
Cyber Security ◽  
Prototype System ◽  
Sequence Matching ◽  
Industrial Control ◽  
State Sequence ◽  
Detection Approach ◽  
Finite State ◽  
Pair Sequence ◽  
Sequence Signatures

This paper discusses two aspects of major risks related to the cyber security of an industrial control system (ICS), including the exploitation of the vulnerabilities of legitimate communication parties and the features abused by unauthorized parties. We propose a novel framework for exposing the above two types of risks. A state fusion finite state machine (SF-FSM) model is defined to describe multiple request-response packet pair sequence signatures of various applications using the same protocol. An inverted index of keywords in an industrial protocol is also proposed to accomplish fast state sequence matching. Then we put forward the concept of scenario reconstruction, using state sequence matching based on SF-FSM, to present the known vulnerabilities corresponding to applications of a specific type and version by identifying the packet interaction characteristics from the data flow in the supervisory control layer network. We also implement an anomaly detection approach to identifying illegal access using state sequence matching based on SF-FSM. An anomaly is asserted if none of the state sequence signatures in the SF-FSM is matched with a packet flow. Ultimately, an example based on industrial protocols is demonstrated by a prototype system to validate the methods of scenario reconstruction and anomaly detection.

Theorem-proving anonymity of infinite-state systems

2007 ◽  
Vol 101 (1) ◽  
pp. 46-51 ◽  
Author(s):  
Yoshinobu Kawabe ◽  
Ken Mano ◽  
Hideki Sakurada ◽  
Yasuyuki Tsukada
Keyword(s):  
Theorem Proving ◽  
Infinite State Systems ◽  
Infinite State
Sign in / Sign up

Export Citation Format

Share Document