Catálogo de publicaciones - libros

This paper focuses on how we can engineer systems so that they can meet their timing requirements. Four separate, but related, issues are addressed: a time band model that caters for the broad set of granularities found in a typical complex system, the delay and deadline statements that allow timing requirements to be specified, scheduling analysis that enables a set of concurrent deadlines to be verified and timing analysis that enables sequential code to be inspected to determine its worst case behaviour. These four topics together with a number of other techniques and tool described in the paper allow real-time behaviour to be delivered.

In this chapter we provide an introduction to the RAISE Specification Language and to the RAISE method. We concentrate on the applicative style of RAISE, the style most commonly used initially in development.

We also describe two examples. The first is a simple communication system that allows the transmission of messages with the possibility of higher priority messages overtaking others. The example illustrates the use of abstract initial specification to capture vital properties, and of more detailed concrete specification to describe a model having those properties. The second example is a control system of a lift, and illustrates the use of model checking to gain confidence in a RAISE model.

In this chapter we will present selected central elements in the theory of Duration Calculus and we will give examples of applications. The chapter will cover syntax, semantics and proof system for the basic logic. Furthermore, results on decidability, undecidability and model-checking will be presented. A few extensions of the basic calculus will be described, in particular, Hybrid Duration Calculus and Duration Calculus with iterations. Furthermore, a case study: the bi-phase mark protocol, is presented. We will not attempt to be exhaustive in our coverage of topics; but we will provide references for further study.

The origins of “formal methods” lie partly in language description (although applications of methods like VDM, RAISE or B to areas other than programming languages are probably more widely known). This paper revisits the language description task but uses operational (rather than denotational) semantics to illustrate that the crucial idea is thinking about an abstract model of something that one is trying to understand or design. A “story” is told which links together some of the more important concepts in programming languages and thus illustrates how formal semantics deepens our understanding.