Code synthesis out of a high-level system behavior models TAT

***Archived: This is a past project,  it is not on offer at the moment!***

Project Description:

The set of regularly used electronic devices in the critical health care aimed to monitor the vital information of the patient has a tendency to be extended with a new class of closed-loop/autonomous devices for patient treatment, for example, periodic drug delivery. Involvement of such devices in the health care process reduces the human factor errors, however, often with the price of introduction of new types of errors due to failures or unpredictable behaviors of the electronic systems. Even one small error of this kind may harm or kill a patient. Therefore, the reliability and safety of the embedded system in this domain comes to the front line among all the requirements to the system properties.

In order to increase the level of reliability and safety of the medical devices we adopt one of the well-known approaches applied in the area of car and airline industries, where safety, reliability and robustness requirements to the embedded systems are not lower than in the medical domain. In this approach the behavior of an embedded system is first modeled using a formal model of computation that is first verified and then automatically transformed into a correct-by-construction executable code. Timed Automata (TA) and its hybrid extension Timed Automata with Tasks (TAT) are well suited for the modeling of real-time systems. The automatic synthesis of the code for a specific platform that preserves the behavior properties of the model must be performed.

The proposed project will include the development of a code generator that would synthesize a C code for the low power RF SoC “IcyCOM” out of a high level system behavior model represented in TAT. The code generator will be based on the previous work where the deterministic semantics of the TAT languages has been defined and a code generator for another specific platform has been designed. The required code generator must be implemented as an extension of the TIMES  tool that supports system modeling with TAT.

Eligibility Requirements:

  • Good programming skills in JAVA and basic C are required;
  • Knowledge of regular expression would help to start with the project;
  • Knowledge of Timed Automata and model checking technics are highly appreciated.

This project was supervised by Dr. Alena Simalatsar  of the Integrated Systems Laboratory (LSI) at EPFL in collaboration with the REDs Laboratory of HEIG-VD, Yverdon-les-Bains. The work formed an important part of the ISyPeM project.

 

***Archived: This is a past project,  it is not on offer at the moment!***