Automating Verification of Non-functional Properties

Abstract : In this deliverable, we document the progress of WP2 during the fourth year of the CONNECT project. Following the last reviews' recommendations, the work is organized into two main streams. One stream concerns a quantitative extension of the compositional specification theory devised during the previous two years, while the other integrates the WP2 CONNECTor algebra with the specification theory so as to support WP3 CONNECTor synthesis. In particular, the assume-guarantee reasoning framework developed for the compositional specification theory ensures that a CONNECTed system preserves global safety properties by just checking the local properties of its constituent components. The proposed quantitative extension of the compositional specification theory allows the modeling of the real-time performance of networked systems, in addition to enabling the synthesis of CONNECTors that are compatible with both the functional behavior and timing constraints of their environments. Finally, in order to integrate the CONNECTor algebra with the specification theory so as to support WP3 synthesis, we defined a method for the automated synthesis of modular CONNECTors. We prove that the behavior of such a CONNECTor is equivalent to the behaviour of a monolithic WP3 CONNECTor. All of the work is evaluated through an application to relevant CONNECT scenarios, e.g., the GMES (Global Monitoring for Environment and Security) scenario.
Type de document :
Rapport
[Research Report] 2012
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00805608
Contributeur : Emmanuelle Grousset <>
Soumis le : jeudi 28 mars 2013 - 13:37:28
Dernière modification le : vendredi 16 septembre 2016 - 15:07:32
Document(s) archivé(s) le : samedi 29 juin 2013 - 04:03:39

Fichier

CONNECT_Deliverable_D2_4.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00805608, version 1

Collections

Citation

Chris Chilton, Lukas Holık, Paola Inverardi, Bengt Jonsson, Marta Kwiatkowska, et al.. Automating Verification of Non-functional Properties. [Research Report] 2012. 〈hal-00805608〉

Partager

Métriques

Consultations de la notice

219

Téléchargements de fichiers

121