Refinement Chart - Using Event-B for Critical Device Software Systems - page 96

Modecharts [ 9 ] is a graphical technique, which is used to handle mode and mode
switching of a system. The authors have given the detailed information about the
state space partition, various working conditions of the system and to define the
control information in the large state machines. However, modecharts lack adequate
support to specifying and reasoning about functional properties. Some papers [ 7 , 13 ]
have also addressed the problem of mode changing in a real-time system. Dotti et
al. [ 6 ] have proposed both formalisation and a refinement notion for a modal system ,
using existing support for the construction of modal system .
According to our literature survey, none of the existing approaches discuss a
refinement-based technique for handling the complexity of a system. We have given
a technique of the refinement chart for presenting different operating modes under
various subsystems. Each subsystem represents an independent function according
to the operating modes. This refinement chart technique helps to design complex
system structure and relationship between two subsystems using operating modes
that helps in system integration using code structuring of the different subsystems.
6.3 Refinement Chart
The purpose of this refinement chart is to specify the modal system requirements in
a form that is easily and effectively implementable. During the modelling of modal
system, several styles of specification are usually adopted for handling the com-
plex operating modes. Functional blocks are divided into multiple simpler blocks in
a new refinement level, without changing the original behaviour of a system. The
final goal is to obtain a specification that is detailed enough to be effectively imple-
mented, but also to correctly describe the requirements of a system.
The development of embedded software for the critical system requires signifi-
cant lower level manual interaction for organising and assembling a complete sys-
tem. This is inherently error-prone, time-consuming and platform-dependent. To
detect the failure cases in a software is not an easy task. Manually reviewing the
source code is the only way to trace the cause of a failure. Due to the technologi-
cal advancement and modern complexity of the critical system software, this is an
impossible task for any third party investigator without prior knowledge of the soft-
ware. Consequently, we have proposed the synthesis of a system using incremental
refinements, to synchronise and integrate the different subsystems of a system. This
approach also helps in code integration and to test the different subsystems of a
system independently.
As the nature of critical systems is often characterisable as modal systems ,we
follow a state-based approach to propose suitable abstractions. We consider that the
state of a model is detailed enough to allow one to distinguish its different operating
conditions and also to characterise required mode functionality and possible mode
switching in terms of state transitions.
Each subsystem that forms the specification is represented into a block diagram
as a refinement chart. Figure 6.1 presents the diagrams of the most abstract modal