Refining EDTL Semantic Classification

Requirements engineering processes are designed to identify and organize requirements for complex software systems. Setting requirements in the form of logical formalisms allows us to automatically check the requirements for programs expressed in the form of transition systems, which guarantees the fulfillment of the required properties on complex combinations of their execution paths and process switchings. Programs and requirements for production control systems are specific and can be described by patterns. In particular, our development of EDTL (Event- Driven Temporal Logic) is designed to set requirements for such systems in the form of a six-component pattern, each component of which describes one of the expected events in the form of a Boolean formula with the addition of changes in system variables along the edges. The general semantics of the requirement can be expressed in the form of a final LTL formula. Having analyzed various requirements for control systems, we discovered that they can be semantically classified into classes, because the final LTL formulas for different requirements can be the same. The paper proposes a semantic classification of formulas for LTL-semantics of the EDTL pattern, based on a combination of constant, equal and complementary logical values of the pattern's attributes.