Formal modelling of environment restrictions from natural-language requirements

Abstract

When creating system models, further to system behaviour one should take into account properties of the environment in order to achieve more meaningful models. Here, we extend a strategy that formalises data-flow reactive systems as CSP processes to take into account environment restrictions. Initially, these restrictions are written in natural language. Afterwards, with the aid of case-grammar theory, they are formalised by deriving LTL formulae automatically. Finally, these formulae are used to prune infeasible scenarios from the CSP-based system specification, in the light of the environment restrictions. Considering examples from the literature, and from the aerospace (Embraer) and the automotive (Mercedes) industry, we show the efficacy of our proposal in terms of state space reduction, up to 61% in some cases.