high integrity design

basics, specification, and refinement

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)

email us  or  telephone   UK: 01625 850 839    International: +44 1625 850 839