Firstly, we extend the Generalised Substitution Language, and therefore the principles of weakest precondition calculus, to embrace differential constraints. Our approach is based on generalising the traditional view that a Generalised Substitution specifies a fragment of a sequential programme. We consider a Generalised Substitution to represent an autonomous transformation which is 'clocked' repeatedly to perform its computation at regular intervals. In the case of such components composed synchronously, we can generalise the notion of weakest precondition to traces (sequences of values) of inputs and outputs. In our approach we characterise traces with first order constraints as 'step' predicates over adjacent elements in the trace. We refer to these as 'acceptance criteria'. We also generalise our calculus to cover nth order differentials. Secondly, we adapt weakest precondition to traces characterised by state machines which represent sequencing constraints. We do this by introducing a form of state machines called 'acceptance machines' which constrain traces of variable values in an alternative way to differential properties. Using the Generalised Substitution Language once more we present a semantics for the propagation of acceptance machines in a manner analagous to predicate transformers. We also use acceptance machines to specify safety properties which have been derived from the safety process. The requirements can then be shown correct with respect to these properties. Finally, we consolidate and integrate our differential calculus and state machine theory with a domain specific formal framework, focusing on the practical application of the theory in a real engineering setting. The domain specific framework which we have selected is Practical Formal Specification. It is a framework which has been developed specifically for use in the engine (and aircraft) control software domain and is based on the decomposition of requirements into components whose usage can be scoped by the specification of environmental and contextual assumptions.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:288811 |
| Date | January 2002 |
| Creators | Blow, James Raymond |
| Publisher | University of York |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
Page generated in 0.0016 seconds