Generalized Substitution Language and Differentials

摘要

Embedded continuous control systems can be thought of as implementing complex (piecewise and pipelined) differential functions. Each `piece' of the function may be preconditioned with a `domain of applicability', which prescribes the circumstances the piece was designed to handle. The preconditions often involve rate of change, i.e. differentials, as well as range constraints. In this paper we present an adaptation of the substitution calculus which can be used to reason about such systems. Our approach is based on generalizing the traditional view that a component is a fragment of a sequential program. We consider a component to be an autonomous transformation which is `clocked' to perform its computation at regular intervals, over and over again. In the case of such a component we can generalize the notion of weakest precondition to traces (sequences of values) of inputs and outputs. In our approach we characterize such traces by `step' predicates over adjacent elements in the trace. We also generalize our calculus to cover n order differentials. Since analysis can be performed at a comparable complexity to regular wp, our techniques are a powerful tool in the validation of continuous control systems.