Bachelor and Master Theses
To apply for conducting this thesis, please contact the thesis supervisor(s).
| Title: | Enabling formal verification of CHESS models by means of model transformations and Rebeca. |
| Subject: | Software engineering |
| Level: | Advanced |
| Description: |
BACKGROUND Modern industrial systems are increasingly complex and require disciplined Software Engineering approaches. Notably, Model-Driven Engineering promotes the use of models to specify the system, analyse as early as possible its quality properties, and consequently guarantee that the current design obeys to the requirements. Eventually, the design shall be mapped towards a corresponding implementation, preferably through automated code generation. CHESS is an Eclipse based open source methodology and toolset adhering to the mentioned MDE principles; it addresses safety, security, reliability, performance, robustness and other non-functional concerns, while guaranteeing correctness of component development and composition for critical embedded systems. CHESS supports the definition of requirements, the modelling of the system functional, logical and physical architecture, down to the software design and its deployment to hardware components. CHESS also features schedulability and dependability analysis functionalities across the life cycle, including back-propagation of analysis results to the model itself (e.g. for fine tuning). OBJECTIVES The goal of this thesis project is extending CHESS with a formal verification approach supported by Rebeca. Rebeca (Reactive Objects Language) is an actor-based language with a formal foundation, designed in an effort to bridge the gap between formal verification approaches and real applications. It can be considered as a reference model for concurrent computation, based on an operational interpretation of the actor model. By going into more details, in order to adhere to the MDE vision underlying the whole methodology, the thesis investigates what is the necessary information to be extracted from CHESS models and to be mapped towards Rebeca specifications in order to perform formal verification. The expected outcomes of the projects are: - an investigation of the CHESS concepts to be extracted in order to perform formal verification in Rebeca such as to guarantee the obtained results for the system; - a mapping procedure to obtain Rebeca specifications from the selected CHESS concepts; - a validation of the proposed solution on a concrete industrial case (provided); - optionally, a model transformation definition to automate the proposed solution. The work shall be adequately documented in a thesis report. Supervisor(s): Antonio Cicchetti (antonio.cicchetti@mdh.se) Examiner: |
| Start date: | |
| End date: | |
| Prerequisites: |
- the thesis project is primarily intended for Advanced Level student(s). The proposal is open to 2 students, and in that case the model transformation definition becomes mandatory. In case we receive only Basic Level candidates we will revise the thesis objectives accordingly; - solid knowledge of UML modelling is required; - Eclipse Modelling Framework knowledge and/or advanced programming skills in Java are highly recommended; - knowledge of MDE and/or Rebeca are a plus. |
| IDT supervisors: | |
| Examiner: | |
| Comments: | |
| Company contact: |