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 commonly studied formalisms are shown to be consistent with this framework. A large example based on an industrial problem is given to demonstrate RD. The integration of system design and management is achieved by unifying formal software engineering methods and model-based reasoning. RD formally specifies a complete toolkit for performing system development and then re-using the development as the system description for diagnostic reasoning. RD does not restrict the contributing system analysis methods, 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 general implementation relation. Implementation relations are widely studied in formal methods in software engineering where they are often referred to as `refinement'. RD allows refinement relations to be defined in a way that makes expected behaviours and faults of system implementations explicit. Furthermore, a case is made that all well known forms of refinement 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 to engineering in general. In particular, a formal engineering process should have benefits beyond just the delivery of systems that satisfy their specifications.
| Identifer | oai:union.ndltd.org:ADTP/215509 |
| Date | January 2006 |
| Creators | de Groot, Martin, Computer Science & Engineering, Faculty of Engineering, UNSW |
| Publisher | Awarded by:University of New South Wales. School of Computer Science and Engineering |
| Source Sets | Australiasian Digital Theses Program |
| Language | English |
| Detected Language | English |
| Rights | Copyright Martin de Groot, http://unsworks.unsw.edu.au/copyright |
Page generated in 0.002 seconds