Flexible Runtime Verification Based On Logical Clock Constraints

Daian Yue 1, 2 Vania Joloboff 1 Frédéric Mallet 3, 4
1 TEA - Tim, Events and Architectures
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
3 AOSTE - Models and methods of analysis and optimization for systems with real-time and embedding constraints
Inria de Paris, CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : We present in this paper a method and tool for the verification of causal and temporal properties of embedded systems, by analyzing the trace streams resulting from virtual prototypes that combines simulated hardware and embedded software. The proposed method makes it possible to analyze different kinds of properties without rebuilding the simulation models. Logical clocks are used to identify relevant points to put observation probes and thus also reducing the trace streams size. We propose a property specification language, called PSML, and based on behavioral patterns that does not require knowledge of temporal logics. From a given PSML specification, simulation is instrumented to generate a trace and the code is dynamically loaded by the simulator. The resulting trace stream is analyzed by parallel automata generated from the specification. The experiments, developed over the SimSoC virtual prototyping framework, show flexibility, possibility of using multi-core platforms to parallelize simulation and verification, providing fast results.
Type de document :
Communication dans un congrès
FDL 2016 - Forum on specification & Design Languages, Sep 2016, Bremen, Germany. 〈https://ecsi.org/fdl〉
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

Contributeur : Frédéric Mallet <>
Soumis le : vendredi 23 décembre 2016 - 10:28:22
Dernière modification le : jeudi 7 février 2019 - 14:48:46
Document(s) archivé(s) le : mardi 21 mars 2017 - 10:50:22


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01421890, version 1


Daian Yue, Vania Joloboff, Frédéric Mallet. Flexible Runtime Verification Based On Logical Clock Constraints. FDL 2016 - Forum on specification & Design Languages, Sep 2016, Bremen, Germany. 〈https://ecsi.org/fdl〉. 〈hal-01421890〉



Consultations de la notice


Téléchargements de fichiers