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

based systems. It is based on the UTP framework [16], and its accompanying
methodology of separation of concerns [7], have been applied in a case study
of a Point Of Sale terminal within the CoCoME (Common Component Mod-
elling Example) challenge [8]. In this paper, we discuss our experience on how
the construction of formal models and their verification and validation can be
integrated in a use case driven and component-based development process. In
particular, we will show with examples from the CoCoME case studies
1. what the models of the different aspects of the systems are at each stage of
the development, including the requirement elicitation , logic design , detailed
design , code generation ,
2. how these models are constructed and derived by application of design pat-
terns that are proved to be a refinement in rCOS, and
3. how verification and validation tasks are identified for the models and what
are the effective tools for these tasks.
With regard to model construction and derivation, we focus on the aspects of
interactions, dynamic behaviour, and static functionality of the system and show
how the design and refinement of constraints on these aspects can be separated,
and how they can consistently form a whole model of the system. For verifica-
tion and validation, we look at consistency between interactions and dynamic
behaviour, component interaction protocols, static analysis and testing of func-
tionality. We discuss how the activities of model construction, transformations,
model verification and validation can be embedded into an existing commer-
cial software development tool, MasterCraft [31]. We have selected this tool,
because it has extensive coverage of the whole software development life-cycle,
from requirements gathering and analysis, through early design stages to imple-
mentation and testing, with support for deployment and maintenance. Finally,
it plays a major role that the producer of MasterCraft, Tata Research Develop-
mentandDesignCentre(TRDDC),generously had permitted us to inspect the
tool in detail.
Overview. The following Section 2 gives an overview on the main ideas and
theme of our research on the rCOS methodology, and provides the formulation
of the main concepts of model-driven development. In Section 3, we demon-
strate, with our recent experience in the work on CoCoME case study, how the
formalization of the concepts, models and techniques developed in rCOS can
be integrated in a model-driven development process. The integration unifies
the different formal techniques of verification and validation with correctness by
design. We then discuss in Section 4 how we can enhance the industrial model-
driven tool, MasterCraft, for the support of the integration of formal design,
verification and validation into a practical engineering development process. Fi-
nally Section 5 summarizes our experience and discusses the plan for our future
work.