Bachelor and Master Theses

Title: Integrating formal analysis techniques into the Progress-IDE
Subject: Computer Science
Level: Advanced
Description: Models and components have become an indispensable part in the development of embedded systems. They reduce the complexity of embedded systems and provide a formal ground on which analysis and synthesis can be performed. ProCom is a component model intended for embedded systems design. It has been developed within PROGRESS, a large research project aiming to provide component-based techniques for the development of embedded systems. An important activity within PROGRESS is to develop an integrated development environment (IDE) in which the different activities of embedded system development can be carried out, ranging from component and system design to analysis, deployment and synthesis. The behavior of ProCom components is specified in the REMES (Resource Model for Embedded Systems) modeling language. REMES is used for specification for both functional and extra-functional behavior of the components (timing, resource usage, etc.). For formal analysis purposes, REMES can be semantically translated into the framework of timed automata or (multi) priced timed automata (PTA) depending on the analysis goals (i.e., timing analysis, resource consumption, etc.). The analysis of PTA is done in the Uppaal Cora tool.

The goal of this thesis is to integrate formal analysis techniques into the Progress-IDE.

In particular the thesis work should include the following tasks:
a) extending the REMES-GUI by extending the REMES metamodel with entry/exit points, declaration of variables and naming of resources. More information about the REMES GUI can be found here:
b) Study the main characteristics of PTA and make a metamodel
c) Study the main characteristics of REMES (REMES metamodel already exist)
d) Compare REMES structural elements and semantics with PTA structural elements and semantics. The comparison between the structural elements can be done on a metamodel level.
e) Design transformation from REMES metamodel to PTA metamodel based on ATL (ATLAS Transformation Language)
f) Analyze and describe the limitations of the transformation
g) Identify the parts that can be automatically transformed and those that require manual transformation
h) Implement the transformation in a tool
i) Integrate the REMES GUI, the transformation and analysis tool (based on Uppaal Cora) into the Progress-IDE through the ProCom atribute framework. More information about the attribute framework can be found here:〈=en&id=0834

Expected outcome:
a) An application that does the transformation from REMES models to PTA models
b) Integration of the REMES GUI, the transformation tool and analysis tool in the Progress-IDE
b) The thesis report describing the work.
Prel. end date: 2011-06-28
Presentation date: 2011-06-28
Student: Dinko Ivanov
IDT supervisor: Aneta Vulgarakis, +46-21-10 73 54
Examinator: Cristina Seceleanu
Cristina Seceleanu, +46-21-151764

Rapport och bilagor


Senaste uppdatering



2011-06-29, 09:56

  • Mälardalen University |
  • Box 883 |
  • 721 23 Västerås/Eskilstuna |
  • 021-101300, 016-153600 |
  • webmaster |
  • Latest update: 2018.05.24