IETS3 + CELT

Model-based Requirements Engineering

Project description

IETS3 and CELT are two independent projects focusing on two different aspects. Goals and outcomes of each project are as following:

IETS3

Software development starts with the requirements gathering process. If the requirements engineering process is not carried out efficiently then it can lead to several potential development issues. Usually companies follow a particular process for requirements gathering that is almost completely manually performed by the requirements engineer. Hence, imposing a large amount of effort to ensure that the gathered requirements are documented in a fashion that is complete, correct and traceable.

The overall goal of the project is to provide innovative and cutting-edge software solutions built on model-based engineering principles focusing on the requirements engineering domain to improve production, quality and cost efficiency for our industrial partners.

To achieve the overall goal there are following sub-goals, mainly development of

  • Domain-specific languages (DSLs) for the requirements domain
  • Analysis for the developed DSLs
  • Automatic synthesis for the developed DSLs
  • Framework for Integrating the developed DSLs and developing mechanisms to guide the requirements engineer to gather requirements that are correct, complete and traceable.

CELT (Cert-mbeddr LighT)

The C language is wide accepted as one of the major development languages in the embedded systems domain. This is because of the fact that the C language is highly expressive and provides flexible syntax and semantics. A problem associated with high expressiveness is that syntactically correct statements that are semantically incorrect can be easily written. Understanding and predicting the semantics of code developed in C is thus an extremely important but difficult task.

The mbeddr stack [1] has been built to address the aforementioned challenge. Mbeddr enables C developers to write C code using a number of abstractions that avoi unnecessary expressiveness, for the embedded system domain. The code written using these abstracts is then converted into real C code using code generators, also called model transformations. However, the generated code has to be verified to ensure the semantics of the code written using the abstracts are preserved in the generated code. This is a crucial issue for the C develops who desires to adopt the mbeddr stack in practice. The main goal of this project is to investigate and develop model-based solutions for verifying the code generation in mbeddr, such that the mbeddr becomes acceptableas one of the options for the C developers to develop the C code for the embedded system domain.

  1. M. Voelter, D. Ratiu, B. Kolb, and B. Schatz. mbeddr: instantiating a language workbench in the embedded software domain. Autom. Softw. Eng., 20(3):339-390,2013

Underlying development technology

We are utilizing MPS (meta-programming editor) for developing our requirements gathering framework and building automatic synthesis mechanisms. The MPS (Meta-Programming System) is a stable industrially-proven projectional meta-editor built by a known software house. MPS uniformly integrates language and editor design capabilities, together with code generation tools and in-built correct-by-construction techniques such as syntax high-lighting, auto-completion or type checking. Easy integration with existing Java libraries adds to the flexibility of this DSL workbench.

Project outcome

IETS3

From this project, our industrial partners will benefit in the form of improvement in their requirements gathering process. Moreover, the provided model-based solutions can partly automate their requirements gathering process and help them gather complete, correct and traceable requirements. This could help them to save effort to manually review the gathered requirements and obtain the appropriate certification from the authorities.

The contributions to date are (non-exhaustive list),

  • Domain-specific languages (DSLs) development

    • Traceability, Glossary and Table languages with Itemis

  • Framework development for integrating the developed languages

    • An extensible framework built based on MIRA framework [1]

  • Semi-automating the requirement gathering process

    • A flow language implemented in the framework implemented as a set of hints to guide the requirements engineer for requirements gathering

  • Development of automatic synthesis of requirements

    • A prototype developed for performing automatic synthesis of requirements for controllers written in EARS+ language before generating controllers software

  1. Sabine Teufl, Dongyue Mou, Daniel Ratiu: MIRA: A tooling-framework to experiment with model-based requirements engineering. RE 2013: 330-331

CELT

The contributions are in a form of deliverables that are:

  • A prototype within mbeddr of a verifiable model-to-model transformation language to replace current model-to-text code generators.
  • A prototype within mbeddr of a pre-/post-condition contract prover for model-to-model transformations expressed in the new transformation language.
  • Reimplementation of a significant share of mbeddr's code generators for the new model-to-model transformation language.
  • A technical argument for the correctness of the implemented code generators. This argument will be built by:
  1. Expressing pre-/post-condition contracts reflecting the expected behavior of mbeddr's code generators.
  2. Using the contract prover in 1. in order to automatically prove or disprove those contracts.

Project Partners

IETS3

CELT

Funding

IETS3 research project is funded by the German Federal Ministry of Education and Research under code 01IS15037A/B

CELT research project is funded by fortiss GmbH and is a fortiss internal project.