A framework for the rigorous design of highly adaptive timed systems

Maxime Cordy, Axel Legay, Pierre Yves Schobbens, Louis Marie Traonouez

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

15 Téléchargements (Pure)

Résumé

Adaptive systems can be regarded as a set of static programs and transitions between these programs. These transitions allow the system to adapt its behaviour in response to unexpected changes in its environment. Modelling highly dynamic systems is cumbersome, as these may go through a large number of adaptations. Moreover, often they must also satisfy real-time requirements whereas adaptations may not complete instantaneously. In this paper, we propose to model highly adaptive systems as dynamic real-time software product lines, where software products are able to change their features at runtime. Adaptive features allow one to design systems equipped with runtime reconfiguration capabilities and to model changes in their environment, such has failure modes. We define Featured Timed Game Automata, a formalism that combines adaptive features with discrete and real-time behaviour. We also propose a novel logic to express real-time requirements on adaptive systems, as well as algorithms to check a system against them. We implemented our method as part of PyECDAR, a model checker for timed systems.

langue originaleAnglais
titre2013 1st FME Workshop on Formal Methods in Software Engineering, FormaliSE 2013 - Proceedings
Pages64-70
Nombre de pages7
Les DOIs
Etat de la publicationPublié - 28 oct. 2013
Evénement2013 1st FME Workshop on Formal Methods in Software Engineering, FormaliSE 2013 - San Francisco, États-Unis
Durée: 25 mai 201325 mai 2013

Une conférence

Une conférence2013 1st FME Workshop on Formal Methods in Software Engineering, FormaliSE 2013
Pays/TerritoireÉtats-Unis
La villeSan Francisco
période25/05/1325/05/13

Empreinte digitale

Examiner les sujets de recherche de « A framework for the rigorous design of highly adaptive timed systems ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation