A Methodology of Eliciting Context Requirements to Program Logic Control Systems
Keywords:
Reactive Systems, Requirement Specification, Linear Temporal Logic, Model Checking, Goal-Oriented Methods of Requirement Development, Problem Frame ApproachAbstract
Purpose: Modern approaches to eliciting formal requirements to software behavior do not provide enough ways to structure
incomplete information about the future system. The paper deals with one of the essential stages in formal verification of software
logical control systems, namely elicitation of temporal requirements. Results: We proposed a technique for eliciting some temporal requirements to logical control software behavior, by modifying problem frames approach. This technique is based on arranging the
temporal relations between events within the system and its operational context. In particular, we considered chains of stimuli and
reactions depending on a source which induces them. In the paper, these temporal relations are called context requirements. Formally,
context requirements have been described in terms of linear temporal logic. We extended the problem frame notation to define ordered
event chains and event blocks, and also added two elementary problem frames, which are temporal relation frame and operational phase
frame. The temporal relation frame can specify problems which require that the system answers by a reactions chain to a stimulus chain
locally. The operational phase frame extends the local behavior determined by the temporal relation frame to the global scope, depending
on the system phase restrictions. Our elementary problem frames can be translated into linear temporal logic formulas. The traditional
problem frame development procedure has been modified to find out context requirements. Practical relevance: The technique has been
demonstrated on the examples of eliciting requirement specifications to two logical control systems (an elevator controller and a vessel
power controller).