Skip to Main content Skip to Navigation
Reports

TRAP: A Platform For Flexible Runtime Verification of Temporal Properties

Daian Yue 1, 2
1 TEA - Tim, Events and Architectures
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : The Trace Runtime Analysis Platform (TRAP) provides a model-based framework and implements the corresponding tool chain to support runtime analysis and verification of traces generated by virtual prototypes or cyber physical systems. The main goal is to make it easy for engineers to define system properties that should be satisfied and verify them at system runtime (or from a recorded session). The property verification tools proposed do not require a detailed knowledge of the system implementation, do not require any modification or recompilation of the system to investigate different properties, and do not require the engineers to be familiar with temporal logic. TRAP proposes Domain Specific Languages (DSL's) integrated within the Eclipse Modeling Framework to express the properties. The DSL toolchain uses the concept of Logical Clock defined by CCSL and takes advantage of CCSL clock algebra as the underlying formal support. The DSL's compilers eventually generate C++ code to verify the properties at run time, making usage of dynamically loaded code.
Document type :
Reports
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-01417075
Contributor : Vania Joloboff <>
Submitted on : Monday, February 13, 2017 - 9:48:34 AM
Last modification on : Friday, January 8, 2021 - 3:12:35 AM
Long-term archiving on: : Sunday, May 14, 2017 - 12:12:19 PM

File

RR-9006 (1).pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01417075, version 1

Citation

Daian Yue. TRAP: A Platform For Flexible Runtime Verification of Temporal Properties. [Research Report] RR-9006, INRIA. 2016, pp.46. ⟨hal-01417075⟩

Share

Metrics

Record views

573

Files downloads

186