Green computing is nowadays a major challenge for most IT organizations. Administrators have to manage the trade-off between system performances and energy saving goals. Autonomic computing is a promising approach to control the QoS and the energy consumed by a system. This paper precisely investigates the use of synchronous programming and discrete controller synthesis to automate the generation of a controller that enforces the required coordination between QoS and energy managers. We illustrate our approach by describing the coordination between a simple admission controller and an energy controller.

We present a technique for designing reconfiguration controllers in the Fractal component-based framework. We obtain discrete control loops that automatically enforce safety properties on the interactions between components, concerning, e.g., mutual exclusions, forbidden or imposed sequences. We use a reactive programming language, with a new mechanism of behavioural contracts. Its compilation involves discrete controller synthesis, which automatically generates the correct adaptation controllers. We apply our approach to the problem of adaptive ressource management, illustrated by the example of a HTTP server.

We describe the extension of a reactive programming language with a behavioral contract construct. It is dedicated to the programming of reactive control of applications in embedded systems, and involves principles of the supervisory control of discrete event systems. Our contribution is in a language approach where modular discrete controller synthesis (DCS) is integrated, and it is concretized in the encapsulation of DCS into a compilation process. From transition system specifications of possible behaviors, DCS automatically produces controllers that make the controlled system satisfy the property given as objective. Our language features and compiling technique provide correctness-by-construction in that sense, and enhance reliability and verifiability. Our application domain is adaptive and reconfigurable systems: closed-loop adaptation mechanisms enable flexible execution of functionalities w.r.t. changing resource and environment conditions. Our language can serve programming such adaption controllers. This paper particularly describes the compilation of the language. We present a method for the modular application of discrete controller synthesis on synchronous programs, and its integration in the BZR language. We consider structured programs, as a composition of nodes, and first apply DCS on particular nodes of the program, in order to reduce the complexity of the controller computation; then, we allow the abstraction of parts of the program for this computation; and finally, we show how to recompose the different controllers computed from different abstractions for their correct co-execution with the initial program. Our work is illustrated with examples, and we present quantitative results about its implementation.

We present a novel technique for designing discrete control loops for adaptive systems. They automatically enforce safety properties on the interactions between tasks, concerning, e.g., mutual exclusions, forbidden or imposed sequences. We use a new reactive programming language, with a mechanism of behavioural contracts. Its compilation involves discrete controller synthesis, which automatically generates the correct appropriate adaptation controllers. We apply our approach to the problem of adaptive ressource management, illustrated by the example of a HTTP server.

We illustrate an approach for the safe design of adaptive embedded systems. It applies the BZR programming language, featuring a special new contract mechanism: its compilation involves automatical discrete controller synthesis. The contribution of this paper is to illustrate how it can be used to enforce the correct adaptation control of the application, meeting execution constraints, with the case study of a video module of a multimedia cellular phone.

This paper presents an approach for the safe design of data-intensive embedded systems. A multimedia application module of last generation cellular phones is considered as a case study. The OMG standard profile MARTE is used to adequately model the application. The resulting model is then transformed into a synchronous program from which a controller is synthesized by using a formal technique, in order to enforce the safe behavior of the modeled application while meeting quality of service requirements. The whole study is carried out in a design framework, GASPARD, dedicated to high-performance embedded systems.

Nous nous intéressons à la conception sûre de systèmes répartis. Nous montrons qu'avec la complexité et l'intégration croissante des systèmes embarqués, la structure fonctionnelle du système peut entrer en conflit avec la structure de son architecture. L'approche traditionnelle de conception par raffinement de cette architecture compromet alors la modularité fonctionnelle du système.

Nous proposons donc une méthode permettant de concevoir un système réparti défini comme un programme unique, dont la structure fonctionnelle est indépendante de l'architecture du système. Cette méthode est basée sur l'ajout de primitives de répartition à un langage flots de données synchrone. Ces primitives permettent d'une part de déclarer l'architecture sous la forme d'un graphe définissant les ressources existantes et les liens de communication existant entre ces ressources, et d'autre part de spécifier par des annotations la localisation de certaines valeurs et calculs du programme.

Nous définissons ensuite la sémantique formelle de ce langage étendu. Cette sémantique a pour but de rendre compte de manière formelle l'effet des annotations ajoutées par le programmeur. Un système de types à effets permet ensuite de vérifier la cohérence de ces annotations. Ce système de types est muni d'un mécanisme d'inférence, qui permet d'inférer, à partir des annotations du programmeur, la localisation des calculs non annotés. Nous définissons ensuite, à partir de ce système de types, une méthode de répartition automatique permettant d'obtenir, à partir d'un programme annoté, un fragment de programme par ressource de l'architecture. La correction du système de types avec la sémantique du langage est prouvée, ainsi que l'équivalence sémantique de l'exécution des fragments obtenus par la méthode de répartition automatique avec le programme initial.

Cette méthode a été implémentée dans le compilateur du langage Lucid Synchrone, et testée sur un exemple de radio logicielle.

This paper addresses the design of distributed systems with synchronous dataflow languages. As modular design entails handling both architecture and functional modularity, we propose a language-oriented solution, involving the extension of a synchronous dataflow language with primitives for program distribution. These primitives allow the programmer to describe the architecture of the system and to express where streams and expressions are located in this architecture. A distributed semantics is first proposed as formalization of the distributed execution of programs. A type and effect system is then provided in order to infer the localization of non-annotated values by means of type inference and to ensure, at compilation time, the consistency of the distribution. A type-directed projection operation allows us to obtain automatically, from a centralized typed program, the local program to be executed by each computing resource. The type system as well as the automatic distribution mechanism has been implemented in the Lucid Synchrone compiler.

This paper shows the application of the automatic distribution of synchronous reactive programs to the specific problem of discrete controller synthesis of complex reactive systems. Discrete controller synthesis is a formal method used to ensure properties on a flexible system which does not a priori verify them. However, this method is efficient only on boolean programs. More complex embedded systems, comprising complex data types and structures, cannot be addressed without abstraction means. We show how such abstractions can be obtained automatically using a type-directed projection operation. This operation allows then the safe recombination of the result of the synthesis with the original abstracted system, preserving the ensured properties.

We propose a simple programming language, called Nemo, specific to the domain of multi-task real-time control systems, such as in robotic, automotive or avionics systems. It can be used to specify a set of resources with usage constraints, a set of tasks that consume them according to various modes, and applications sequencing the tasks. We obtain automatically an application-specific task handler that correctly manages the constraints (if there exists one), through a compilation-like process including a phase of discrete controller synthesis. This way, this formal technique contributes to the safety of the designed systems, while being encapsulated in a tool that makes it useable by application experts. Our approach is based on the synchronous modelling techniques, languages and tools.

Keywords: real-time systems, safe design, domain-specific language, discrete control synthesis, synchronous programming