Formal Specification of Non-Functional Properties of Context-Aware Systems

Introduction

Context-Aware Systems refer to a category of software systems that can automatically adapt their behavior at run-time as a response to changes in the surrounding context. One major challenge in designing such systems is to provide sufficient and appropriate layers of abstraction to ensure independent specification for software entities and their provided services from parts related to adaptation (context and its management). In this context, Component-Based Software Engineering (CBSE) is viewed as an opportunity to deal with the increasing complexity of context-aware software. However, by moving to the component-based area (Vale et al., 2016), new challenges and obstacles appear such as maintaining the global consistency of the component-based models. Therefore, all relevant properties of software components must be precisely and formally described.

In conventional model-based development work-flows (Ray et al., 2011), design models are first constructed and then verified against functional requirements (specifications of what the system must or must not do). Otherwise, requirements related to the non-functional aspects of system behavior are typically reasoned about, if at all, in a specific adhoc manner, despite that it is critical to ensure correct and unambiguous system behavior. Falling to meet any property can lead to system failure in satisfying internal business, users, or market needs or do not fulfill mandatory qualities imposed by clients. Few conceptual models offer mechanisms for modeling and validating non-functional requirements. A commonly accepted approach to the semantics of such requirements is also missing. Therefore, developing a semantic framework to model and design context-aware systems as well as verifying their inherent properties by ensuring both functional and non-functional correctness are major issues. Recently, many studies have concentrated on the expression of functional and non- functional properties, but they lack formality and precise semantics. The context-aware computing community increasingly recognizes the benefits of formal methods (Han & Youn, 2012) in the description of static and dynamic features of computing environments, as well as the verification of correctness properties of both the specification and the system prototype. Rewriting logic (Meseguer, 1992) via its implementation language Maude (M. Clavel et al., 2005) is an adequate candidate for the definition of the semantic basis of non-functional properties framework.

Authors objective through the present work is to present a formal framework for the specification and validation of non-functional requirements, taking into account the specific needs of a context-aware system. The proposed framework provides customized concepts to integrates non-functional requirements design and validation in the development process. Based on these semantic concepts, a formal semantics is then associated via the definition of a formal specification language: CTXs-Maude (for ConTeXt-aware Systems using Maude). The concrete syntax of CTXs-Maude language is then associated with an operational semantics that makes its specification executable. Hence, providing a formal simulation of system execution and offering systems designers the ability to perform automatic verification and validation of non-functional properties. Diverse terms have been used to refer to non-functional requirements. Some of them are “constraint”, “quality attributes”, “non-functional properties”, “quality of service”, “requirements” or “non-behavioral requirements”. This variability of terms about non-functional requirements comes from vocabularies of different domains, like software engineering, distributed systems or service-oriented programming (Belhajjame et al., 2018). In the case of context-aware systems, non-functional requirements concern the context in which the application is executed, the condition of triggering an adaptation as well as quality constraints imposed by the services. In this paper authors use Non-Functional Properties (NFPs) to refer to context-aware systems non-functional concepts.