A framework for the rigorous design of highly adaptive timed systems

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

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

13 Downloads (Pure)

Abstract

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.

Original languageEnglish
Title of host publication2013 1st FME Workshop on Formal Methods in Software Engineering, FormaliSE 2013 - Proceedings
Pages64-70
Number of pages7
DOIs
Publication statusPublished - 28 Oct 2013
Event2013 1st FME Workshop on Formal Methods in Software Engineering, FormaliSE 2013 - San Francisco, United States
Duration: 25 May 201325 May 2013

Conference

Conference2013 1st FME Workshop on Formal Methods in Software Engineering, FormaliSE 2013
CountryUnited States
CitySan Francisco
Period25/05/1325/05/13

Keywords

  • Features
  • Model-checking
  • Real-time systems
  • Software Product Lines
  • Timed Games

Fingerprint Dive into the research topics of 'A framework for the rigorous design of highly adaptive timed systems'. Together they form a unique fingerprint.

Cite this