Compositional Verification for Timed Systems Based on Automatic Invariant Generation

Autor: Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga, Jacques Combaz

Publikováno v: Logical Methods in Computer Science, Vol Volume 11, Issue 3 (2015)

We propose a method for compositional verification to address the state space explosion problem inherent to model-checking timed systems with a large number of components. The main challenge is to obtain pertinent global timing constraints from the t

Externí odkaz: https://doaj.org/article/cab2ce2fce42464191d052bf3eaec61a

Runtime Verification of Timed Properties in Autonomous Robots

Autor: Saddek Bensalem, Mohammed Foughali, Jacques Combaz, Félix Ingrand

Publikováno v: 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)
18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), ACM/IEEE, Dec 2020, Jaipur (virtual), India. ⟨10.1109/MEMOCODE51338.2020.9315156⟩
MEMOCODE

International audience; Throughout the last few decades, researchers and practitioners are showing more and more interest in using formal methods in order to predict and prevent software failures in robotic and autonomous systems. However, the applic

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3009f6f483332a6727699350493ebcf5
https://hal.science/hal-03093298

Performance Evaluation of Stochastic Real-Time Systems with the SBIP Framework

Autor: Jacques Combaz, Marius Bozga, Axel Legay, Braham Lotfi Mediouni, Ayoub Nouri, Saddek Bensalem

Publikováno v: International Journal of Critical Computer-Based Systems
International Journal of Critical Computer-Based Systems, Inderscience, In press, pp.1-33
International Journal of Critical Computer-Based Systems, In press, pp.1-33
International Journal of Critical Computer-Based Systems, Vol. 8, no.3/4, p. 340 (2018)

International audience; The SBIP framework consists of a stochastic real-time component-based modelling formalism and a statistical model checking engine. The former is built as a stochastic extension of the real-time BIP formalism and enables the co

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2d55a36c21fad36f53e228d0c8aa0a04
https://hal.archives-ouvertes.fr/hal-01898426

Rigorous implementation of real-time systems – from theory to application

Autor: Tesnim Abdellatif, Joseph Sifakis, Jacques Combaz

Publikováno v: Mathematical Structures in Computer Science. 23:882-914

The correct and efficient implementation of general real-time applications remains very much an open problem. A key issue is meeting timing constraints whose satisfaction depends on features of the execution platform, in particular its speed. Existin

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b703bf9af2c6874d79c8b5bfbd27fd60
https://doi.org/10.1017/s096012951200028x

RTD-Finder: A Tool for Compositional Verification of Real-Time Component-Based Systems

Autor: Saddek Bensalem, Marius Bozga, Souha Ben-Rayana, Jacques Combaz

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783662496732
TACAS
Lecture Notes in Computer Science
22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016)
22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), Apr 2016, Eindhoven, Netherlands. pp.394-406, ⟨10.1007/978-3-662-49674-9_23⟩

International audience; In this paper we present RTD-Finder, a tool which applies a fully compositional and automatic method for the verification of safety properties for real-time component-based systems modeled in the RT-BIP language. The core meth

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::bb409159885d824bdb5666f5463e23e9
https://doi.org/10.1007/978-3-662-49674-9_23