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

different kinds of operating modes, and decompose the whole system based on oper-
ational modes. Decomposing using the refinement chart helps to analyse individual
component and interaction or switching from one operating mode to other operating
modes. Formal verification and validation are carried out by both formal modelling
experts and domain experts (medical experts and control engineers), while refine-
ment chart based system integration approach and system development are carried
out by industrial people.
6.5 Summary
Today, in order to respect the certifiable assurance and safety, time to market and
strict cost constraints, critical system designers need some new modelling and sim-
ulation solutions. The solutions must also permit software component modelling,
component integration in a distributed environment, easier debugging of complex
specifications, and mitigated connection with other, existing or new systems [ 10 ].
In this chapter, we would like to stress the original contribution of our work. At
each refinement step, some functional blocks are divided into simpler blocks, with-
out changing the behaviour of a system is represented by the refinement chart. We
have proposed a technique to synthesis, integrate, and synchronise the subsystems
of a system using incremental refinements. This approach helps in code integration
and to test the different subsystems independently. The purpose of the refinement
chart is to provide an easily manageable representation for different refinement sub-
systems. The refinement chart offers a clear view of assistance in the system in-
tegration. This is an important issue not only for being able to derive system-level
performance and correctness guarantees, but also for being able to assemble compo-
nents in a cost-effective manner. Moreover, the refinement chart represents a block
diagram for each subsystems and provides a structure in various refinements to build
the complete system. Concrete refinement charts provide system integration infor-
mation in the form of compose and decompose of software codes according to the
blocks diagrams. Composition and decomposition help to improve the code struc-
ture and code optimisation. To find a minimum set of events for each independent
subsystem is known as code optimisation, and synthesising and synchronising of
a set of events are known as code structuring. The refinement chart specially cov-
ers component-based design frameworks and decomposition, integration of critical
infrastructure and device integration. The complexity of design is reduced by struc-
turing systems using modes and by detailing this design using refinement.
References
1. Abrial, J.-R. (1996). The B-book: Assigning programs to meanings . New York: Cambridge
University Press.
2. Abrial, J.-R. (2010). Modeling in Event-B: System and software engineering (1st ed.). New
York: Cambridge University Press.