In some situations we have to be particularly careful that our software
does what we need it to do.
-
Safety or security critical systems
-
Embedded systems, where recall or update of the software would be very
expensive
-
Frameworks and component architectures on which many systems will be based
-
Components that will be used in many applications, or will be used in their
creation (such as compilers)
There is a variety of tactics that can be brought to bear to ensure reliability,
including especially rigorous testing régimes, analysis of the code
for properties such as liveness, and adherence to strict design standards.
Among the most effective techniques are rigorous specification and traceable
refinement.
Rigorous specification means writing unambiguous abstract models (avoiding
implementation detail) against which the program code can b measured. It's
equivalent to writing all the test harnesses before beginning coding; though
a much more succinct language can be used.
Traceable refinement means documenting exactly why the design is believed
to meet the spec. As part of testing the code, we write a number of 'refinement
relations' that implement the mapping between the abstract model and the
code.
Catalysis for specification and refinement
Specification and refinement have a long history: the VDM and Z methods
date from the nineteen-eighties. Catalysis adapts these approaches to object
and component based programming, and uses the UML notation.
Catalysis is compatible with relevant MIL and ISO standards, and is
in use by a variety of projects in, for example, Loral Federal Systems,
and Eurofighter.
complete solutions for high integrity design with Catalysis
(consultancy, courses, workshops, mentoring, seminars, development)