Model checking temporal properties of reaction systems

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.

Download Full-text

Verification of Linear-Time Temporal Properties for Reaction Systems with Discrete Concentrations

Fundamenta Informaticae ◽

10.3233/fi-2017-1567 ◽

2017 ◽

Vol 154 (1-4) ◽

pp. 289-306 ◽

Cited By ~ 4

Author(s):

Artur Męski ◽

Maciej Koutny ◽

Wojciech Penczek

Keyword(s):

Linear Time ◽

Reaction Systems ◽

Temporal Properties

Download Full-text

Model-Checking Temporal Properties of Real-Time HTL Programs

Lecture Notes in Computer Science - Leveraging Applications of Formal Methods, Verification, and Validation ◽

10.1007/978-3-642-16561-0_22 ◽

2010 ◽

pp. 191-205

Author(s):

André Carvalho ◽

Joel Carvalho ◽

Jorge Sousa Pinto ◽

Simão Melo de Sousa

Keyword(s):

Model Checking ◽

Real Time ◽

Temporal Properties

Download Full-text

BDD-based Bounded Model Checking for Temporal Properties of 1-Safe Petri Nets

Fundamenta Informaticae ◽

10.3233/fi-2011-513 ◽

2011 ◽

Vol 109 (3) ◽

pp. 305-321 ◽

Cited By ~ 1

Author(s):

Artur Męski ◽

Wojciech Penczek ◽

Agata Półrola

Keyword(s):

Model Checking ◽

Petri Nets ◽

Bounded Model Checking ◽

Temporal Properties

Download Full-text

Chapter 18. Bounded Model Checking

Frontiers in Artificial Intelligence and Applications - Handbook of Satisfiability ◽

10.3233/faia201002 ◽

2021 ◽

Author(s):

Armin Biere

Keyword(s):

Model Checking ◽

Design Automation ◽

Electronic Design Automation ◽

Industrial Applications ◽

Bounded Model Checking ◽

Hardware Verification ◽

Considerable Part ◽

Temporal Properties ◽

Electronic Design

One of the most important industrial applications of SAT is currently Bounded Model Checking (BMC). This technique is typically used for formal hardware verification in the context of Electronic Design Automation. But BMC has successfully been applied to many other domains as well. In practice, BMC is mainly used for falsification, which is concerned with violations of temporal properties. In addition, a considerable part of this chapter discusses complete extensions, including k-induction and interpolation. These extensions also allow to prove properties.

Download Full-text