So, you are a Phd candidate…. You mean student, right?

Before I start, I would like to say that this post is based on my own experience while I was a Phd candidate and reflects my opinion about what is a Phd. It's amazing how this misunderstanding happens a lot. People usually associate "jobs" to when you are producing something tangible and "studying" otherwise. It's …

Going Beyond with a Disk-Based Model Checker

What about exploring 3 billion states using only 13G of Ram? Yes, you read right, this is what the new option "disc_async" is capable of. Our new disk-based algorithm is able to explore large graphs using less RAM memory and going as fast as the classical sequential RAM based algorithm (DISK:27690  instead of RAM:25017 seconds). …

The Syntax and Semantics of FIACRE

Abstract: This document presents the syntax and formal semantics of the Fiacre language, version 3.0. Fiacre is an acronym for Format Intermediaire pour les Architectures de Composants Répartis Embarqués (Intermediate Format for the Architectures of Embedded Distributed Components). Fiacre is a formal intermediate model to represent both the behavioral and timing aspects of systems —in …

Observation Graph implementation for TINA toolbox

Abstract: Model Checking is a formal technique for the verification of finite systems. However, it is well known that this technique suffers from the state explosion problem. We describe work in progress to implement in the TINA toolbox an enumerative variant of a state based observation graph algorithm defined by Klai and Poitrenaud. Authors: Rodrigo …

Enumerative Parallel and Distributed State Space Construction

Abstract: Model Checking requires high-end computers to verify complex systems. Consequently, it is interesting to use multi-processors architecture in order to have more computational resources available to deal with bigger models. This work presents a survey of parallel and distributed state space construction for Model Checking purpose. Authors: Rodrigo Tacla Saad, Bernard Berthomieu, Silvano Dal …

A General Lock-Free Algorithm for Parallel State Space Construction

Abstract: Verification via model-checking is a very demanding activity in terms of computational resources. While there are still gains to be expected from algorithmic improvements, it is necessary to take advantage of the advances in computer hardware to tackle bigger models. Recent improvements in his area take the form of multiprocessor and multicore architectures with …

Mixed Shared-Distributed Hash Tables Approaches for Parallel State Space Construction

Abstract: We propose an algorithm for parallel state space construction based on an original concurrent data structure, called a localization table, that aims at better spatial and temporal balance. Our proposal is close in spirit to algorithms based on distributed hash tables, with the distinction that states are dynamically assigned to processors, i.e. we do …

An Experiment on Parallel Model Checking of a CTL Fragment

Abstract: We propose a parallel algorithm for local, on the fly, model checking of a fragment of CTL that is well-suited for modern, multi-core architectures. This model-checking algorithm benefits from a parallel state space construction algorithm, which we described in a previous work, and shares the same basic set of principles: there are no assumptions …

What Is Model Checking ???

Maybe you have already heard about the technique "Model Checking".  Maybe not... Anyway, What is model checking??? Model checking is a valuable formal verification method that can be used to avoid the presence of logical errors. In that respect, model checking contributes to improving the safety of embedded systems (and also to improve the level …