True Concurrency Semantics

The model checking algorithms have been widely studied for timed automata, it's a validation technique for automatically verifying correctness properties of finite-state systems, which are based on interleaving semantics. Therefore the actions are assumed instantaneous. To overcome the hypothesis of temporal and structural atomicity of actions, we use the durational actions timed automata model (daTA). This model is based on the maximality semantics. Properties to be verified are expressed using the Timed Computation Tree Logic (TCTL). For dealing with formal verification, the Maximality-based Region Graph (MRG) is defined and an adaptation of the model checking algorithm is proposed. The use of the maximality semantics based verification provides new class of properties related to simultaneous progress of actions at different states.

Download Full-text

Safety Assurance of a High Voltage Controller for an Industrial Robotic System

Lecture Notes in Computer Science - Formal Methods: Foundations and Applications ◽

10.1007/978-3-030-63882-5_4 ◽

2020 ◽

pp. 45-63

Author(s):

Yvonne Murray ◽

David A. Anisi ◽

Martin Sirevåg ◽

Pedro Ribeiro ◽

Rabah Saleh Hagag

Keyword(s):

Model Checking ◽

Formal Verification ◽

High Voltage ◽

Software Tool ◽

Safety Requirements ◽

Safety Assurance ◽

Voltage Controller ◽

Finite State ◽

Low Threshold ◽

The Comparative Study

Abstract Due to the risk of discharge sparks and ignition, there are strict rules concerning the safety of high voltage electrostatic systems used in industrial painting robots. In order to assure that the system fulfils its safety requirements, formal verification is an important tool to supplement traditional testing and quality assurance procedures. The work in this paper presents formal verification of the most important safety functions of a high voltage controller. The controller has been modelled as a finite state machine, which was formally verified using two different model checking software tools; Simulink Design Verifier and RoboTool. Five safety critical properties were specified and formally verified using the two tools. Simulink was chosen as a low-threshold entry point since MathWorks products are well known to most practitioners. RoboTool serves as a software tool targeted towards model checking, thus providing more advanced options for the more experienced user. The comparative study and results show that all properties were successfully verified. The verification times in both tools were in the order of a few minutes, which was within the acceptable time limit for this particular application.

Download Full-text

Formal Verification of Heuristic Autonomous Intersection Management Using Statistical Model Checking

Sensors ◽

10.3390/s20164506 ◽

2020 ◽

Vol 20 (16) ◽

pp. 4506

Author(s):

Aaditya Prakash Chouhan ◽

Gourinath Banda

Keyword(s):

Model Checking ◽

Statistical Model ◽

Formal Verification ◽

Autonomous Vehicles ◽

Timed Automata ◽

Autonomous Systems ◽

Statistical Model Checking ◽

Stage Of Development ◽

Verification Techniques ◽

Intersection Management

Autonomous vehicles are gaining popularity throughout the world among researchers and consumers. However, their popularity has not yet reached the level where it is widely accepted as a fully developed technology as a large portion of the consumer base feels skeptical about it. Proving the correctness of this technology will help in establishing faith in it. That is easier said than done because of the fact that the formal verification techniques has not attained the level of development and application that it is ought to. In this work, we present Statistical Model Checking (SMC) as a possible solution for verifying the safety of autonomous systems and algorithms. We apply it on Heuristic Autonomous Intersection Management (HAIM) algorithm. The presented verification routine can be adopted for other conflict point based autonomous intersection management algorithms as well. Along with verifying the HAIM, we also demonstrate the modeling and verification applied at each stage of development to verify the inherent behavior of the algorithm. The HAIM scheme is formally modeled using a variant of the language of Timed Automata. The model consists of automata that encode the behavior of vehicles, intersection manager (IM) and collision checkers. To verify the complete nature of the heuristic and ensure correct modeling of the system, we model it in layers and verify each layer separately for their expected behavior. Along with that, we perform implementation verification and error injection testing to ensure faithful modeling of the system. Results show with high confidence the freedom from collisions of the intersection controlled by the HAIM algorithm.

Download Full-text

Model checking of finite-state machine-based scenario-aware dataflow using timed automata

10th IEEE International Symposium on Industrial Embedded Systems (SIES) ◽

10.1109/sies.2015.7185065 ◽

2015 ◽

Cited By ~ 6

Author(s):

Mladen Skelin ◽

Erik Ramsgaard Wognsen ◽

Mads Chr. Olesen ◽

Rene Rydhof Hansen ◽

Kim Guldstrand Larsen

Keyword(s):

Model Checking ◽

Finite State Machine ◽

Timed Automata ◽

State Machine ◽

Finite State

Download Full-text

Compositional Model Checking of Real Time Systems

BRICS Report Series ◽

10.7146/brics.v2i19.19921 ◽

1995 ◽

Vol 2 (19) ◽

Cited By ~ 2

Author(s):

Francois Laroussinie ◽

Kim G. Larsen

Keyword(s):

Model Checking ◽

Timed Automata ◽

Parallel Composition ◽

Combinatorial Explosion ◽

Binary Decision ◽

Practical Applications ◽

Compositional Model ◽

Finite State ◽

Time Systems ◽

Combined Technique

A major problem in applying model checking to finite-state systems is the potential combinatorial explosion of the state space arising from parallel composition. Solutions of this problem have been attempted for practical applications using a variety of techniques. Recent work by Andersen [And95] proposes a very promising compositional model checking technique, which has experimentally been shown to improve results obtained using Binary Decision Diagrams. In this paper we make Andersen's technique applicable to systems described by networks of timed automata. We present a quotient construction, which allows timed automata components to be gradually moved from the network expression into the specification. The intermediate specifications are kept small using minimization heuristics suggested by Andersen. The potential of the combined technique is demonstrated using a prototype implemented in CAML.

Download Full-text