Portal de Periódicos da CAPES

A predicative semantics for real-time refinement

2003; Springer Nature; Linguagem: Inglês

10.1007/978-0-387-21798-7_6

0172-603X

Ian J. Hayes,

Model-Driven Software Engineering Techniques

Real-time systems play an important role in many safety-critical systems. Hence it is essential to have a formal basis for the development of real-time software. In this chapter we present a predicative semantics for a real-time, wide-spectrum language. The semantics includes a special variable representing the current time, and uses timed traces to represent the values of external input and outputs over time so that reactive control systems can be handled. Because a real-time control system may be a nonterminating process, we allow the specification of nonterminating programs and the development of nonterminating repetitions. We present a set of refinement laws covering the constructs in the language. The laws make use of a relational style similar to that of Cliff Jones, although they have been generalised to handle nonterminating constructs.