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

Building on existing software certification standards, such as IEC-62304 and the
Common Criteria [ 15 , 22 , 34 ], more and improved approaches which use formal
methods in software certification are needed. Applying these new approaches for
highly critical systems should have many benefits; the exposure of errors which
might have not been detected without formal methods. That guidance, as proposed
by NITRD, IEEE, and IEC/ISO [ 28 , 35 , 36 ], allows adoption of formal methods into
an established set of processes for the development and verification of a critical sys-
tem to be an evolutionary refinement rather than an abrupt change of methodology.
Formal methods might be used in a very selective manner to partially address a small
set of objectives, or might be the primary source of evidence for the satisfaction of
many of the objectives concerned with development and verification.
Two reliable facts of formal methods have demonstrated by last decades of re-
search and experience—they are not the “ silver bullet ” to eliminate all software
failures, but neither are they beyond the budget constraints of software develop-
ers. In critical system, formal methods are commonly demonstrating the absence
of undesired behaviours and preserving essential properties. Model checkers, theo-
rem provers, real-time animation and automatic code generation make it possible to
analyse the complexity of the system and produce the final implemented system. On
the other hand, the ability to generate complete test cases from formal specifications
can result in overall savings, despite the cost of developing the specification. The
process of developing a specification is often the most valuable phase of a formal
verification, and “lightweight formal methods” approaches make it possible to for-
mally analyse partial specifications and early requirements definitions. Experience
with mandated use of formal techniques and other standards provides empirical ev-
idence that these methods can be successfully incorporated into the development
process for the critical systems. Remaining chapters include detailed descriptions
of the new associated techniques and tools, which are used in this development
methodology for critical system development.
References
1. Abrial, J.-R. (2010). Modeling in Event-B: System and software engineering (1st ed.). New
York: Cambridge University Press.
2. Abrial, J.-R., Börger, E., & Langmaack, H. (Eds.) (1996). Lecture notes in computer science:
Vol. 1165 . Formal methods for industrial applications, specifying and programming the steam
boiler control . Berlin: Springer.
3. Acuña, S. T., & Juristo, N. (2005). International series in software engineering. Software
process modeling . Berlin: Springer.
4. Badeau, F., & Amelot, A. (2005). Using B as a high level programming language in an indus-
trial project: Roissy VAL. In H. Treharne, S. King, M. Henson, & S. Schneider (Eds.), Lecture
notes in computer science: Vol. 3455 . ZB 2005: Formal specification and development in Z
and B (pp. 15-25). Berlin: Springer.
5. Basili, V. R., & Turner, A. J. (1975). Iterative enhancement: A practical technique for software
development. IEEE Transactions on Software Engineering , 4 , 390-396.
6. Bell, R., & Reinert, D. (1993). Risk and system integrity concepts for safety-related control
systems. Microprocessors and Microsystems , 17 , 3-15.