A Formal Model for Natural-Language Timed Requirements of Reactive Systems

To analyse the behaviour of reactive systems formally, it is necessary to build a model. At the very beginning of the development, typically only natural language requirements are documented. We present a formal model, named Data-Flow Reactive Systems (DFRS), which can be automatically obtained from natural language requirements that may also describe temporal properties. We prove that a DFRS can be mapped to a timed input-output transition system, which is widely used to characterise conformance relations for timed reactive systems. To validate the proposed model as well as the mechanisation developed to support its analysis, we consider two toy examples and two examples from the aerospace and automotive industry. Test cases are independently created and we verify that they are all compatible.