A formal approach for the specification and verification of trustworthy component-based systems

Abstract

Software systems are increasingly becoming ubiquitous affecting the way we experience the world. Embedded software systems, especially those used in smart devices, have become an essential constituent of the technological infrastructure of modern societies. Such systems, in order to be trusted in society, must be proved to be trustworthy. Trustworthiness is a composite non-functional property that implies safety, timeliness, security, availability, and reliability. This paper presents a formal approach for the development of trustworthy component-based systems. The approach involves a formal component model for the specification of component’s structure, functional, and non-functional (trustworthiness) properties, a model transformation technique for the automatic generation of component behavior using the specified structure and restricted by the specified properties, and a unified formal verification method for safety, security, reliability and availability properties using model checking.

Introduction

A trustworthy system is one on which we can depend upon, by placing a full measure of trust in its abilities to perform as expected. Trustworthiness is a moral value concept which implies commitment and ability to be relied and depended on. The social aspect of trust is hard to define formally. It is a relation between two parties in which the trusting party places confidence, reliance, and dependence, whereas the trustee commits to take responsibility and never betray the trust. In computing literature, trustworthiness is defined as the system property that denotes the degree of user confidence that the system will behave as expected (Schneider et al., 1999, Avizienis et al., 2004). The terms trustworthiness and dependability are used interchangeably (Sommerville, 2007). Dependability is defined as “the ability to deliver services that can justifiably be trusted” (Avizienis et al., 2004). A comparison between the two terms presented in (Avizienis et al., 2004) has concluded that the two properties are equivalent in their goals and address similar concerns. The goals of dependability are providing justifiably trusted services and avoiding outage of service that is unacceptable to the consumer. The above definitions emphasize the importance of justifying trust. In order to justify trust, we should define trustworthiness formally.

Our everyday living experience with the technological infrastructure surrounding us provides a motivation to formulate a meaning for trust in computing. We use elevators everyday although they may fail to provide service on some day and occasionally will behave in unsafe modes. We travel in airplanes which are being controlled fully by autopilot, a software that guides the aircraft. Modern day cars that we drive contain up to one gigabyte of embedded software and 67 processors that implement around 270 user functions with which we interact (Pretschner et al., 2007). These systems are typical examples of complex embedded systems, the class of real-time reactive systems in which the responses to a stimulus may be strictly regulated by timing constraints. They maintain continuous interaction with their environment through stimulus and response, and their ubiquitous nature affect the way we experience life and perform work. Because they perform a complex set of operations in safety-critical contexts, a formal analysis of their behavior must be conducted before declaring their trustworthiness. This paper’s contribution fits this need. We discuss a rigorous development methodology involving formal verification for developing systems of the above kind and provide a formal approach to verify their specified trustworthiness properties.

There is a common consensus (Schneider et al., 1999, Avizienis et al., 2004, Mundie et al., 2002) that trustworthiness is a composite concept and that the essential quality properties contributing to trustworthiness are safety, security, reliability, and availability. Timeliness is inherent in the quality attributes of safety, reliability, and availability. Past research in specifying and verifying safety and security properties and estimating reliability and availability properties at system architectural level have progressed only independently. This is due to many reasons such as (1) the early finding that safety and security properties cannot be formally specified, composed, and verified together in any one formal method (McLean, 1996), (2) the conventional ways of estimating reliability at a system architecture using stochastic methods which are based on uncertain and inaccurate parameters (Gokhale, 2007), and (3) the lack of research in analyzing availability (Immonen and Niemelä, 2008). There is no published work that we are aware of which successfully combined all these attributes in one formal approach. In order to develop trustworthy systems, all these properties must be combined together in one formal approach. This paper provides a novel formal approach based on component-based development (CBD) for developing trustworthy systems. Our approach enables the specification and verification of safety, security, reliability, and availability properties using a unified component model.

Component-based development (CBD) is the type of software engineering development in which systems are built by constructing units, called components, that perform simple tasks, and assembling them to create composite components that perform complex tasks. CBD promises many advantages to software development including reuse, managing complexity, and reducing the development’s time, effort, and cost. CBD is widely adopted in software industry as the mainstream approach to software engineering (Sommerville, 2007). It is increasingly used to develop software systems, especially embedded systems, deployed in safety-critical environments. Component model is an essential constituent of CBD. A component model defines what components are (their syntax and semantics), their composition to develop component-based systems, and their deployment (Lau and Wang, 2007). A component is defined as “a software element that conforms to a component model and can be independently deployed and composed without modification according to a composition standard” (Heineman and Councill, 2001). Components provide and require services through public interfaces. The provided services are the operations performed by the component. The required services are the operations that the component needs in order to complete its provided services and produce results. The interfaces of a component provide specification of the public services that are provided and required by the component.

Component specification should include both functional and non-functional requirements. However, current component models have limited or no support for specifying non-functional requirements. For enhancing reuse non-functional requirements and environmental constraints should be defined as contracts at the interfaces of a component. This is because when environmental assumptions and non-functional requirements are packaged together in components, they cannot be used in different deployment environments. For example, in real-time embedded systems time constraints that define the maximum amount of time for a safe execution of a service might be different depending on hardware and software configurations of the deployment environment. The separation between the computation part of the component and its contract enables components to be reused in different environments by changing only its contract. However, when studying current component models, there is limited or no support for contracts. Moreover, a study of current component models (Lau and Wang, 2007) reveals that composition is defined using direct method calls or indirect message passing through connectors. As a result tightly coupled components are produced that are difficult to reuse. Also, when assembling components, special composition rules should be applied to ensure that the non-functional requirements of the constituent components are preserved in the assembly. This requires a defined composition theory. However, there is no component model that defines a composition theory for both the structural and non-functional parts of components (Lau and Wang, 2007). Furthermore, when analyzing the current component models in the literature, we find that very few of them support real-time requirements. In this paper we put forth a new component definition which enables reuse of trustworthy components in embedded software systems.

This paper is a contribution to the challenges of defining trustworthy components, composing trustworthy components, and verifying trustworthiness in a unified model. The main contributions are the following:

• As part of a formal definition of trustworthiness safety, security, reliability and availability properties are formalized. A formal definition of trustworthy components is given. This definition can be adopted by other component models to enhance their support for trustworthiness. Structural, functional, and non-functional requirements, specially the properties of trustworthiness, are formalized. The formal model includes a contract in which the relations between components and the trustworthiness properties are specified.

• A composition theory is given. It postulates rules for composing both the structural requirements and the trustworthiness properties. A composition is driven by the required services of a component. A formal proof is given to show that a composition of two trustworthy components is trustworthy.

• An automatic transformation process is given. It generates behavior models and real-time models from formal component definitions.

• Based upon component formalism it is shown that it is possible to use one formal verification technique for safety, security, reliability, and availability properties. UPPAAL model checking tool is used for formal verification, and Times tool is used for real-time schedule analysis.

• Two industrial strength case studies, in their simplified form, are discussed. These are

  • the steam boiler controller problem (Abrial et al., 1996), a benchmark case study for modeling real-time systems, and

  • CoCoME (Rausch et al., 2008), a common component modeling example introduced by the component development community for comparing and evaluating different component modeling techniques.

The rest of this paper is organized as follows: Section 2 introduces the formal definition of trustworthy components. Section 3 presents a model transformation approach for the automatic generation of component behavior and real-time models based on the formal definitions of components. Section 4 introduces a novel qualitative approach for the specification and verification of reliability and availability properties. Section 5 presents a demonstration of our formal methodology using two case studies. Section 6 presents comparison between our work and the related work in the literature. Finally, Section 7 provides concluding remarks and directions to future work.