Bachelor and Master Theses

Title: Automated Transformation of Requirements from Natural language to Formal specification
Subject: Computer Science
Level: Basic or Advanced (contact supervisor)
Description: Background and Thesis Goal
In most embedded systems, such as automotive systems, software requirements are usually written in unconstrained natural language, e.g., English. Since natural language (NL) is inherently ambiguous, unintentional mistakes might occur in the NL specification, resulting in erroneous software requirements. Such potential errors lead to undesirable system behaviors after implementation, which are costly to detect and resolve at that late stage. Therefore, it is desirable to have means of transforming the NL requirements into formally specified ones, e.g. requirements expressed in a formal logic, which can be analyzed against a system model, for instance by model checking, at early development stages.

A formal specification is a mathematical representation of a requirement. For instance, in Computation Tree Logic (CTL), the following requirement :
"AG (a_switch_pressed --> AF light_bulb_is_On)", means
"It is Always the case that Globally, if a switch is pressed (a_switch_pressed) then it is Always the case that Finally the light bulb shall be ON (light_is_On)".
Such specifications are not easy to produce or understand by non-specialists, but they can be automatically generated and interpreted by software tools, such as the UPPAAL model checker.

This thesis aims at developing, implementing and validating an algorithm for the automatic transformation of ReSA requirements into Computation Tree Logic, and its timed version.

Current status
Our research team developed a constrained natural language (that is a subset English) for writing requirements in automotive systems, known as Requirements Specification Language (ReSA). Writing requirements in ReSA can reduce ambiguity; however, it cannot be used as such in formal analysis of requirements, and verification of formal architectural models. Therefore, a subset of ReSA will be transformed into a formal specification language, that is into (T)CTL, by an automatic procedure, in order to be later fed into a model checker.

Research questions
(1) What are the existing techniques for the automatic transformation of requirements in natural language to their formal specification?
(2) How can software requirements be transformed automatically from ReSA into (Timed) Computation Tree Logic (TCTL)?
(3) Is the proposed automatic transformation ReSA2(T)CL applicable on industrially-sized systems?

Expected outcomes
Expected outcomes of the thesis includes:
(1) A transformation algorithm from requirements in ReSA to requirements in (T)CTL.
(2) An implementation of the algorithm in the ReSA tool, and the solution’s validation on an industrial use case, from VGTT.
(3) A thesis report describing the above.

Company: MDH, kontaktperson: Nesredin Mahmud
Start date: 2016-09-15
Prel. end date: 2017-01-30
Student: Linus Järvela
Prerequisites: Programming in Java, Eclipse framework is plus
IDT supervisor: Cristina Seceleanu, +46-21-151764
Misc: ReSA, and TCTL lecture link:

Rapport och bilagor


Senaste uppdatering

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