Critical System Development Methodology - Using Event-B for Critical Device Software Systems - page 60

Chapter 4
Critical System Development Methodology
Abstract Formal methods have emerged as an alternative approach to ensuring the
quality and correctness of the high confidence critical systems, overcoming limi-
tations of the traditional validation techniques such as simulation and testing. This
chapter presents a methodology for developing critical systems from requirement
analysis to automatic code generation with standard safety assessment approach.
This methodology combines the refinement approach with various tools including
verification tool, model checker tool, real-time animator and finally, produces the
source code into many languages using automatic code generation tools. This ap-
proach is intended to contribute to further the use of formal techniques for devel-
oping the critical systems with high integrity and to verify the complex properties,
which help to discover potential problems.
4.1 Introduction
Software quality assurance for critical systems is an emerging market. New tools
and techniques are developed to provide an assurance that systems will never show
any failure. These tools and techniques are used for designing critical systems like
avionics, medical devices and automotive. New developed tools and techniques are
varied according to the diversity in critical systems. For example, in the medi-
cal domain, small systems like a pacemaker, requires different kinds of tools and
Sections of this chapter are adapted from the original publication: Méry, D., & Singh, N. K.
(2012). Critical systems development methodology using formal techniques. In Proceedings
of the third symposium on information and communication technology , SoICT'12, Ha Long
(pp. 3-12). New York: ACM.
ACM COPYRIGHT NOTICE. Copyright © 2012 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] .