Reasoning about designs: a framework for coupling formal developments and system management

This thesis presents a framework for formal system development. The framework is called `RD' which is short for`Reasoning about Designs'. RD integrates proof, development and diagnostic modes of reasoning. Many commonlystudied formalisms are shown to be consistent with this framework. A large example based on an industrial problem isgiven to demonstrate RD.The integration of system design and management is achieved by unifying formal software engineering methods andmodel-based reasoning. RD formally specifies a complete toolkit for performing system development and then re-using thedevelopment as the system description for diagnostic reasoning. RD does not restrict the contributing system analysismethods, rather it maps out and defines the entities and relations common to both. The framework is, in principle,extensible to support other forms of reasoning.The ground technical mechanism of the framework is a novel view of formal system development based on a generalimplementation relation. Implementation relations are widely studied in formal methods in software engineering where theyare often referred to as `refinement'. RD allows refinement relations to be defined in a way that makes expectedbehaviours and faults of system implementations explicit. Furthermore, a case is made that all well known forms ofrefinement implicitly support diagnostic reasoning as they can be restated within the framework.RD is an integrated and completely rigorous approach to the core system building tasks of design and management.Despite the large amount of technical detail, the following discussion can be seen as raising many issues that relate toengineering in general. In particular, a formal engineering process should have benefits beyond just the delivery ofsystems that satisfy their specifications