Semantic Classification of Event Driven Temporal Logic Requirements

The process of requirements engineering involves the elaboration of requirements for complex software systems. In our series of works, we consider formalized requirements, which can later be used in the process of formal verification of software system models. For reactive control programs that respond to events from sensors, we have previously proposed to express the requirements in a tabular form as a tuple of Boolean logic formulas. This form constituting a logical pattern with a given linear-time temporal semantics specific to control programs is much clearer than standard temporal logic formulas. However, we found that if one defined constant values instead of formulas in some cells of our table then the final formula can be significantly simplified. Moreover, different combinations of possible variants of cell values can correspond to the same resulting formulas. In this paper, we analyze classes of such formulas by implementing software to simplify the linear-time temporal logic formulas. This approach can be used to obtain a natural language representation of the requirements originally specified formally, with the goal that such representations have a minimal form.