Consistency Checking of Functional and Non‐Functional Requirements in Self‐Adapting Systems

ABSTRACT Background A self‐adaptive software system adapts its structure and behavior in response to changes. It manages run‐time changes that are difficult to predict and check at design time before deployment. It may also change its requirements and goals according to its environment. This work presents an approach to specify and verify a self‐adaptive software architecture. The aim is to ensure that the software, after adaptation, conforms to the requirements specification with respect to functional and nonfunctional constraints. Methods The proposed approach is based mainly on the use of a sequence diagram of the unified modeling language (UML) to specify the software interactions and requirements along with nonfunctional constraints. Whenever an adaptation event is received, this sequence diagram is consequently adapted and then transformed into communicating timed automata in order to be checked by the UPPAAL (UPPsala and AALborg universities) model checking tool. Results The proposed approach allows software architecture to adjust itself or its requirements and run‐time changes without stopping its execution. Conclusions This approach provides a solution that helps maintain the coherence and consistency of self‐adaptive software architecture before, during, and after adaptation. We illustrate our proposed approach by applying it to a case study.