Diplomarbeit/Masterarbeit: Incremental Development for Critical Systems Using Certificates

13.09.2010, Abschlussarbeiten, Bachelor- und Masterarbeiten

The goal of this master thesis is to support incremental changes in a development process based on models and their properties – provided as certificates. Main parts of the thesis are: - Developing a format for specifications. It will be based on invariants, temporal logics formula. - Choosing an analysis tool and implementing a certificate generation and checking environment. The implementation will be based on an existing Java Eclipse environment. This comprises among other features a parser and a meta model. - Developing a small case study to evaluate the approach.

The goal of this master thesis is to study the relation between models and their properties – provided as certificates -- during incremental changes in a development process. Given the following use-case: A software developer starts a development process with some initial model and initial specification of its properties. A certificate generator and checker is used to ensure the validity of these properties (certification). Both model and properties are refined during the development process. The refinement is based on the results of the certificate generator and checker and implemented by the software developer.

Work Plan: Based on existing tools, a certificate generator and checker will be realized in this thesis. This certificate generator will analyze the system and discover properties and encapsulate them in a machine readable certificate. The certificate generator will support an incremental development process: it will be able to reuse old certificates from previous development cycles and adapt them to changes. Possible modeling languages (based on background or previous experience one will be chosen at the beginning of the thesis) comprise IEC 61131-3 (an industrial standard) or BIP (a modeling language for concurrent systems). Important tasks that have to be taken care of in this thesis comprise:
- Developing a format for specifications. It will be based on invariants, temporal logics formula.
- Choosing an analysis tool and implementing a certificate generation and checking environment. The implementation will be based on an existing Java Eclipse environment. This comprises among other features a parser and a meta model.
- Developing a small case study to evaluate the approach.


Prerequisites: Interest in formal methods and modeling languages.
Responsible supervisor (Aufgabensteller) PD Dr. habil. Bernhard Schätz
Advisor and contact (Betreuer und Ansprechpartner) Dr. Jan Olaf Blech (blech@fortiss.org)

Kontakt: blech@fortiss.org