A HIGHER LEVEL OF BEHAVIORAL SPECIFICATION - AN EXAMPLE IN INTERVAL TEMPORAL LOGIC

This paper reports on the use of Moszkowski's Tempura - an executable version of Interval Temporal Logic - in developing behavioral specifications for digital circuits. A Tempura model for a commercial avionics circuit is described, showing how Tempura facilitates a well-structured executable specification, incorporating timing characteristics, but expressed at a high level of abstraction. A second version shows the use of temporal projection to develop a model at a finer temporal granularity.