Lacramioara Astefanoaei ; Souha Ben Rayana ; Saddek Bensalem ; Marius Bozga ; Jacques Combaz
-
Compositional Verification for Timed Systems Based on Automatic
Invariant Generation
Compositional Verification for Timed Systems Based on Automatic
Invariant GenerationArticle
Authors: Lacramioara Astefanoaei ; Souha Ben Rayana ; Saddek Bensalem ; Marius Bozga ; Jacques Combaz
NULL##NULL##NULL##NULL##NULL
Lacramioara Astefanoaei;Souha Ben Rayana;Saddek Bensalem;Marius Bozga;Jacques Combaz
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 timings in the components alone. To this end, we make use
of auxiliary clocks to automatically generate new invariants which capture the
constraints induced by the synchronisations between components. The method has
been implemented in the RTD-Finder tool and successfully experimented on
several benchmarks.
CErtification of Real Time Applications desIgNed for mixed criticaliTY; Funder: European Commission; Code: 288175
Autonomic Service-Component Ensembles; Funder: European Commission; Code: 257414
Bibliographic References
5 Documents citing this article
Imene Ben Hafaiedh, 2019, A generic formal model for the comparison and analysis of distributed job-scheduling algorithms in grid environment, Journal of Parallel and Distributed Computing, 132, pp. 331-343, 10.1016/j.jpdc.2019.05.002.
Maroua Ben Slimane;Imene Ben Hafaiedh;Riadh Robbana, 2017, Formal-Based Design and Verification of SoC Arbitration Protocols: A Comparative Analysis of TDMA and Round-Robin, IEEE Design and Test, 34, 5, pp. 54-62, 10.1109/mdat.2017.2713352.
Imen Ben Hafaiedh;Maroua Ben Slimane;Riadh Robbana, Lecture notes in computer science, A Distributed Formal Model for the Analysis and Verification of Arbitration Protocols on MPSoCs Architecture, pp. 658-674, 2016, 10.1007/978-3-319-49583-5_51.
Mahieddine Dellabani;Jacques Combaz;Marius Bozga;Saddek Bensalem, Lecture notes in computer science, Local Planning of Multiparty Interactions with Bounded Horizons, pp. 199-216, 2016, 10.1007/978-3-319-48989-6_13.