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

Chapter 6
Refinement Chart
Abstract Refinement techniques serve as a key role for modelling a complex sys-
tem in an incremental way. This chapter also presents a required technique namely
refinement chart for handling the complexity of a system. Refinement chart is a
graphical representation of a complex system using layering approach, where func-
tional blocks are divided into multiple simpler blocks in a new refinement level,
without changing the original behaviour of the system. The main objective of this
refinement chart is to model the whole system using graphical notations and to ob-
tain a concrete specification. The refinement chart offers a clear view of assistance
in “system” integration. This approach also gives a clear view about the system as-
sembling based on operating modes and different kinds of features. To show the
effectiveness of this approach, we have used this graphical modelling technique to
simplifying the complexity of a system in the development of our selected case
study: cardiac pacemaker.
6.1 Introduction
High-confidence medical devices (ICD, pacemaker, infusion pump, etc.), automo-
tive and avionic systems are too much error prone in operating due to the complex-
ity of the systems [ 3 , 5 , 12 ]. New methodologies are needed to make critical viable
in the future marketplace by simplifying the various design stages. This chapter
Sections of this chapter are adapted from the original publication: Méry, D., & Singh, N. K.
(2013). Formal specification of medical systems by proof-based refinement. ACM Transactions
on Embedded Computing Systems , 12 (1), 15:1-15:25.
ACM COPYRIGHT NOTICE. Copyright © 2013 by the Association for Computing Machinery,
Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom
use is granted without fee provided that copies are not made or distributed for profit or
commercial advantage and that copies bear this notice and the full citation on the first page.
Copyrights for components of this work owned by others than ACM must be honored.
Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to
redistribute to lists, requires prior specific permission and/or a fee. Request permissions from
Publications Dept., ACM, Inc., fax [phone], or [e-mail] .