Advanced features of Duration Calculus and Sequential Hybrid Programs

摘要

This paper adds a number of advanced features into DC, and aims to provide a semantical framework for sequential hybrid programs. In particular, 1. A higher order hiding operator is introduced to model local variables in real-time programs. 2. A relational composition is formed to model the sequential composition operator of programming languages. 3. Neighbourhood values of state variables are used to represent the stable states of program variables. We have shown that the super-dense chop is the product of the ITL chop and the relational composition operator, where the former models the sequential composition of continuously evolving physical environment, and the latter composes discrete computing agents. This paper also presents a link between the theory of designs and DC. It enables us to discuss time-independent properties of real-time programs in untimed refinement calculus, and as a result greatly simplifies the reasoning task for hybrid systems. In this paper, the advanced features of DC are employed in formalising SHP, and provide verification methods for reasoning timing properties. The same notations have been used to tackle concurrent real-time systems, and provide a denotational semantics for an industrial specification language.