Harnessing rCOS for Tool Support—The CoCoME Experience - Formal Methods and Hybrid Real-Time Systems - page 84

requires a large team of people playing different roles and carrying out differ-
ent activities of design, construction, analysis, verification and validation. The
management of the development process is complex, too.
In practical software engineering nowadays, complexity is dealt with by a
component-based and model-driven development process [7,9] where
1. the different aspects and views of the system are described in a UML-like
multi-view and multi-notational language, and
2. separation of design and validation of different concerns is supported by
design patterns, object-oriented and component-based designs.
However, there are no rigorous unified theories and tools which support specifi-
cation, verification and validation of the models produced in such a process.
Rigorous verification and validation of a software system requires the ap-
plication of formal methods. This needs a formal version of the requirements
specification, and the establishment of a property to imply that the specified
requirement holds as long as the assumptions hold. The assumptions are specifi-
cations for or constraints on the behavior of environment and system elements.
In the past half a century, semantic foundations, formal notations and techniques
and tools of verification and validation have been developed, including testing ,
static analysis , model checking , formal proof and theorem proving ,and runtime
checking . They can be classified into the following frameworks:
- event-based models [29,15] are widely used for specification and verifica-
tion of interactions, and are supported by model checking and simulation
tools [30,2].
- pre-post conditions and Hoare logic are applied to specifications of function-
ality and static analysis. These are supported by tools of theorem proving,
runtime checking and testing [22,11,28].
- state transition systems and temporal logics are popular for specification and
verification of dynamic control behaviours. They are supported by model
checking tools [17,21].
However, each framework is researched mostly by a separate community, and
most of the research in verification has largely ignored the impact of design
methods on feasibility of formal verification. Therefore, the formal techniques
and tools are not good with regard to scalability and they are not easy to be
integrated into practical design and development processes. The notion of pro-
gram refinement [4] has obvious links to the practical design of programs with
the consideration of abstraction and correctness, but the existing refinement cal-
culi are shown to be effective only for small imperative programs. There is a lack
of a formal foundation for object-oriented and component-based model refine-
ment until the recent work on formal methods of component and object systems
[10,25,14,6].
The formalism, rCOS [14,6], that we have recently developed, is a rather rich
and mature formalism that models static and dynamic features for component