Formal Methods for Characterization and Analysis of Quality Specifications in Component-based Systems

TL;DR

This paper introduces a formal, compositional framework for analyzing and assessing the quality attributes of component-based systems, facilitating design exploration and ensuring system reliability.

Contribution

It presents a novel formal framework for quality analysis of component-based systems, including formal specifications, query-driven assessment, and design exploration tools.

Findings

Framework effectively computes quality attributes for various system structures.

Formal query-driven assessment aids in exploring and optimizing component configurations.

Case study demonstrates practical applicability and benefits of the proposed approach.

Abstract

Component-based design paradigm is of paramount importance due to prolific growth in the complexity of modern-day systems. Since the components are developed primarily by multi-party vendors and often assembled to realize the overall system, it is an onus of the designer to certify both the functional and non-functional requirements of such systems. Several of the earlier works concentrated on formally analyzing the behavioral correctness, safety, security, reliability and robustness of such compositional systems. However, the assurance for quality measures of such systems is also considered as an important parameter for their acceptance. Formalization of quality measures is still at an immature state and often dictated by the user satisfaction. This paper presents a novel compositional framework for reliable quality analysis of component-based systems from the formal quality specifications of its constituent components. The proposed framework enables elegant and generic computation methods for quality attributes of various component-based system structures. In addition to this, we provide a formal query-driven quality assessment and design exploration framework which enables the designer to explore various component structures and operating setups and finally converge into better acceptable systems. A detailed case-study is presented over a component-based system structure to show the efficacy and practicality of our proposed framework.