4.1 (Ana)Tempura

Tempura, the C-Tempura interpreter version 2.7 developed originally by Roger Hale and now maintained by Antonio Cau and Ben Moszkowski, is an interpreter for executable Interval Temporal Logic formulae. The first Tempura interpreter was programmed in Prolog by Ben Moszkowski, and was operational around December 2, 1983. Subsequently he rewrote the interpreter in Lisp (mid Mar, 1984), and in late 1984 modified the program to handle a two-level memory and multi-pass scanning. The C-Tempura interpreter was written in early 1985 by Roger Hale at Cambridge University.

AnaTempura, which is built upon C-Tempura, is a tool for the runtime verification of systems using Interval Temporal Logic (ITL) and its executable subset Tempura. The runtime verification technique uses assertion points to check whether a system satisfies timing, safety or security properties expressed in ITL. The assertion points are inserted in the source code of the system and will generate a sequence of information (system states), like values of variables and timestamps of value change, while the system is running. Since an ITL property corresponds to a set of sequences of states (intervals), runtime verification is just checking whether the sequence generated by the system is a member of the set of sequences corresponding to the property we want to check. The Tempura interpreter is used to do this membership test.

Download Version:

How to run AnaTempura?

Contact: Email cau.researcher@gmail.com in case of problems.


Overview: Figure 1 shows an overview of AnaTempura.

Figure 1: Overview of AnaTempura

Figure 2 shows the interface of AnaTempura.

Figure 2: Interface of AnaTempura

Figure 3 shows a graphical snapshot of a simulation of the EP/3 microprocessor specified in Tempura.

Figure 3: Graphical snapshot of simulation of the EP/3 microprocessor

Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023