An approach to support incremental software construction and verification in component-based system development

Component-based System Development (CBSD) is a promising way of thinking or philosophy to reduce the cost and time of software system development. Moreover, CBSD is able to tame the complexity of today’s software systems development while the quality is guaranteed. However, supporting correctness and building trust in CBSD are of great importance to detect errors as early as they appear. It is commonly acknowledged that formal specification and verification methods are reliable methods that are able to offer fundamental aid to reveal errors and increase confidence in designing software systems. One of the approaches to verify systems is model checking. It is a brute-force verification method which is able to automatically and systematically analyze the state space and formal properties of a given system to discover hidden faults. However, it is limited by State Space Explosion (SSE). The amount of State Space (SS) of a given system tends to increase dramatically and quickly exceed the memory capacity even for a small system. Many techniques and approaches have been proposed to deal with SSE. They commonly try to circumvent SSE after the entire system is constructed. Among them, there is the incremental model checking which verifies systems before the construction is completed. The incremental verification style has been introduced in model checking of CBSD and it is considered suitable for the implicit style of model checking. However, the explicit style is not supported before in model checking of CBSD. In this thesis, a verification approach is proposed to support the incremental verification of CBSD that is considered suitable for explicit model checking. The proposed approach is provided through three main steps in preparing a component model, constructing systems incrementally, and integrating verification into the incremental construction. In the first step, a new component model called PUTRACOM is proposed. Components in PUTRACOM support encapsulation in the sense that computation is completely private. It has been achieved by adding Observer/Observable Unit (OOU) in the components. This feature leads to minimized coupling between the components in the systems and facilitate incremental construction. To compose components new exogenous connectors are introduced. The substantial feature of the exogenous connectors is encapsulating all controls in the system. Combining the new connectors with OOU provides a way to prevent having multiple ports and let the computation part of components be truly encapsulated. In the second step, an approach to construct systems incrementally is proposed. The technique emphasizes on iteratively constructing and enhancing an approach version of a system by adding new increments. To achieve this, the provision of new conditions and rules is essential to maintain the system behavior during construction. A set of definitions, rules and conditions are introduced to define the system’s behavior, explore the entire system to find them, and proof their preservation in each level of construction. The applicability of the approach is also elaborated by an example. In the third step, an approach to integrate a verification process into the levels of constructions is proposed. The approach is able to avoid re-verifying lower level of constructions and lesses the state space size and verification effort via deleting the encapsulated part of each component. The approach is specified through steps, definitions and rules. Its applicability is verified by performing the rules on implementing on a real world case study. The utilized real world case study is CoCoME which implemented in Colored Petri Net (CPN) Tools. It demonstrates how PUTRACOM provides a way to construct encapsulated components, control interactions between them by new connectors, incrementally construct and verify systems, and reduce verification efforts. The results indicate that the proposed technique can reduce the amount of state space to be checked in the component-based development. Consequently, the reduction of the state space leads to reduce the amount of execution time during the verification process. Moreover, the counterexamples can be found as early as it appears