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...
Saved in:
| Main Author: | |
|---|---|
| Format: | Thesis |
| Language: | English |
| Published: |
2019
|
| Subjects: | |
| Online Access: | http://psasir.upm.edu.my/id/eprint/90768/1/FSKTM%202019%2056%20IR.pdf |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Summary: | 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. |
|---|