Vérification Dynamique de Propriétés Temporelles

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.La plateforme d’analyse de trace en runtime TRAP fournit un outillage dans le cadre de l’ingénierie dirigée par les modèles qui permet l’analyse et la vérification de traces pour des prototypes virtuels et des systèmes cyber-physiques. Le principal objectif est de faciliter la définition de propriétés qui doivent être satisfaites, et leur vérification soit pendant le fonctionnement du système, soit sur des traces enregistrées. Les outils de vérification proposés n’exigent pas de connaître dans les détails l’implémentation du système, et aucune recompilation ou reconstruction du système n’est nécessaire pour explorer différentes propriétés. Les langages proposés ne requièrent pas non plus de connaissance préalable de la logique temporelles pour ceux qui les manipulent. TRAP propose des Langages Spécifiques de Domaine (DSL) intégrés dans les outils Eclipse. Ces langages reposent sur le formalisme CCSL avec sa notion d’horloge logique et l’algèbre d’horloges associée. Les compilateurs des langages génèrent du code C++ qui vérifie les propriétés temporelles en faisant usage de chargement dynamique de code