| || |
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
Download Stable Version:
- Version 3.0 (released 04/07/2013) gzipped tar file or zip file.
- Dropped pre-compiled Solaris binary.
- flex/bison based parser backward compatible with previous hard coded
version but with stricter syntactic checks
- changed from cvs to svn as version control system
- improved syntax error messages
- fixed memory leaks
- tidy up format command
- startup file .anatempurarc can also be in the current directory
- use kbs-0.4.4 to generate anatempura binaries
- anatempura binaries are using Tcl/Tk 8.6
- works again under Windows XP
- program assertions can have any symbol except control characters and !
- Version 2.18 (released 01/11/2012): gzipped tar file or zip file.
- Dropped tempura_macosx binary but added tempura_linux64 and
- fixed some small bugs
- fixed memory leaks
- added command ‘winput’ that will wait for input from a file instead
of switching to the keyboard.
- Version 2.17 (released 04/10/2011): gzipped tar file or zip file.
- initial support for MACOSX
- fixed gui bugs
- fixed some tempura bugs
- Version 2.16 (released 08/12/2009): gzipped tar file or zip file.
- added floats. Floats have the form $2.3e+10$ in Tempura. For output:
output($2.3$) will be $2.30000e+00$ , i.e., precision is 5 digits
after the ’.’. One can set this via the precision variable. With
precision of 2 one gets $2.30e+00$. The format command can output
floats in two forms: %f output will be of the form 2.33333, e output
will be of the form 2.33333e+01. The following operations on floats
are defined: unary, +, -; binary: +, -, div, mod, /, *, **, ceil,
floor, sqrt, itof, exp, log, log10, sin, cos, tan, asin, acos, atan,
atan2, sinh, cosh, tanh, fabs.
- anatempura is now using the new Tile interface
- when setting system variables with set, output both old and new
- Added ’frandom’ and ’fRandom’ for float random number between
- Added defaults command, X defaults 1 denotes when X is undefined
then take as value for X the value 1.
- Added prev(X) operator, the value of X in the previous state.
- Added mem(X) operator, X is a ’memory’ variable, i.e., when
undefined take the value in the previous state.
- Added #n history operator, used as option to exists when declaring a
variable, it will keep a history of n previous values of a variable.
- Added nprev(X,n) operator, nprev(X,3) for instance is an
abbreviation of prev(prev(prev(X))).
- When setting debug_level to 6 more usefull information is displayed
like the state of a variable and reduction rule being applied.
- Included tempura executables tempura_linux for Linux (compiled on
Ubuntu 9.10), tempura_solaris for Solaris (compiled on Sparc
Solaris 10u8), and tempura.exe for Windows (compiled on Windows XP SP3).
- Included anatempura executables anatempura_solaris, anatempura_linux
and anatempura.exe. These were built using the Tclkit Kitgen build
system (http://wiki.tcl.tk/18146). Now no need anymore to install
tcl/tk and expect in order to run anatempura.
- changed copyright license to GPLv3.0
- Version 2.15 (released 14/08/2008): gzipped tar file or zip file.
- introduced various node accessor macros so that if one changes the node
structure we only have to change the macro.
- if formula can’t be reduced in the final state of the
prefix of a chop then we will evaluate ((prefix and empty);true)
and (suffix). This feature can be switched on/off with hopchop.
The default of hopchop is true.
- added integer overflow tests.
- unified/cleaned up the various node data structures.
- Version 2.14 (released 29/11/2007): gzipped tar file or zip file.
- work around a recent misfeature of windows when started an external program.
- added the io redirections, set infile="some file name", set
outfile="some file name", where stdin and stdout can be used to
redirect to standard keyboard and screen i/o.
- added the infinite and randlen constructs for respectively an
infinite interval and a random length interval (less or equal
- Version 2.13 (released 28/08/2007): gzipped tar file or zip file.
- added reset in file menu to restart tempura.
- open and reload now also load the file into Tempura.
- added showstate Tempura command. This will display what is
(un)defined in the current state.
- changed contact email address to email@example.com
- Version 2.12 (released 04/05/2007): gzipped tar file or zip file.
This version is the first version that compiles both under
Windows and Unix/Linux type of machines. See Changelog for detailed
To run the graphical interface you can either
- use the pre-compiled binary:
anatempura_linux (Ubuntu 12.04, 32 bits)
anatempura_linux64 (Ubuntu 12.04, 64 bits)
anatempura.exe (Windows XP, Windows 7)
- or use anatempura.tcl:
you need to compile tempura, install Tcl/Tk (at least 8.5) and Expect. You can get
Tcl/Tk from Tcl/Tk site and you can get Expect from the Expect homepage. A
convenient way of installing these is using the ActiveTcl package which includes both.
ActiveTcl is the complete, ready-to-install Tcl/Tk distribution for Windows, Mac OS
X, Linux, Solaris, AIX and HP-UX. Newer versions of the ActiveTcl do not
have the Expect package installed. But you can get Expect with the teacup
(For Windows you have to do this in a DOS shell.)
Type the following command:
teacup install Expect
Tempura can be compiled using the Gnu C compiler under a Unix like operating system
like Ubuntu, GNU Debian, etc. For Windows you need to install the MinGW
(Minimalist GNU for Windows). For convenience the pre-compiled binary for Windows
(Windows XP, Windows 7) and for Linux (Ubuntu 12.04, both 32 and 64 bits) are
Email firstname.lastname@example.org in case of problems.
- Analysing C programs is discussed in:
A Framework For Analysing The Effect of ‘Change’ In Legacy Code, S. Zhou, H.
Zedan and A. Cau. In IEEE Proc. of ICSM’99, 1999.
- Analysing Verilog programs is discussed in:
A logic-based Approach for Hardware/Software Co-design, H. Zedan and A. Cau.
Digest of IEE event Hardware-Software Co-design, 8 Dec., 2000.
- A paper describing the run-time verification method used in AnaTempura:
Run-time analysis of time-critical systems. S. Zhou and H. Zedan and A. Cau. Journal
of System Architecture, 51(5):331-345, 2005.
- Slides of seminar talk about AnaTempura:
AnaTempura, A. Cau, S. Zhou and H. Zedan.
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
Figure 3: Graphical snapshot of simulation of the EP/3 microprocessor
6.2 ITL Theorem Prover based on Prover9
Prover9 is a resolution/paramodulation automated theorem prover for first-order and equational
logic developed by William McCune.
We have given an algebraic axiom system for Propositional Interval Temporal Logic (PITL):
Interval Temporal Algebra. The axiom system is a combination of a variant of Kleene algebra
and Omega algebra plus axioms for linearity and confluence.
This algebraic axiom system for PITL has been encoded in Prover9. So we can
use Prover9 to prove the validity of various PITL theorems. The Prover9 encoding
of PITL plus examples of more than 300 PITL theorems are available for download
- Version 1.8 (released 27/08/2009): gzipped tar file.
- documentation updated to new semantics for
chopstar and chop omega algebraic operators
- Version 1.7 (released 15/05/2009): gzipped tar file.
- updated documentation in doc, to use new ITL semantics
- Version 1.6 (released 12/12/2008): gzipped tar file.
- changed copyright license to GPLv3.0 and added the notice to all files
- Version 1.5 (first public release: 05/12/2008): gzipped tar file.
The README in this tar file contains instructions how to use Prover9 for proving PITL
6.3 FLCheck: Fusion Logic decision Procedure
Fusion Logic augments conventional Propositional Temporal Logic (PTL) with the fusion
operator. Note: the fusion-operator is basically a “chop” that does not have an explicit negation
on the left hand (for right fusion logic) side (as fusion expression) or the right hand (for left
fusion logic). The negation is implicit, i.e., the negation is a derived fusion expression operator.
The expressiveness of Fusion Logic is the same as Propositional Interval Temporal Logic. The
main differences concern computational complexity, naturalness of expression for analytical
purposes, and succinctness. Fusion Logic is closely related to Propositional Dynamic Logic
We have implemented above decision procedure for Fusion Logic (html pages containing
details) in Tcl/Tk and the CUDD BDD library. The tool allows one to check the validity or
satisfiability of a Fusion Logic formula. If a formula is not valid it will produce a counter example
and if a formula is satisfiable it will produce an example model. Figure 4 gives a screen dump of
our tool which is available at
Figure 4: FLCHECK fusion logic decision procedure
6.4 ITL Proof Checker based on PVS
PVS is an interactive environment, developed at SRI, for writing formal specifications and
checking formal proofs. The specification language used in PVS is a strongly typed higher order
logic. The powerful interactive theorem prover/proof checker of PVS has a large set of basic
deductive steps and the facility to combine these steps into proof strategies. PVS is
implemented in Common Lisp –with ancillary functions provided in C, Tcl/TK and
LaTeX– and uses GNU Emacs for its interface. PVS is freely available for IBM RS6000
machines as well as Sun Sparcs under license from SRI. See PVS homepage for more
6.5 Automatic Verification of Interval Temporal Logic
Shinji Kono has developed an automatic theorem prover for propositional ITL (LITE). The
implementation is in Prolog. Further information can be gathered at Shinji Kono’s Interval
Temporal Logic page. Shinji Kono has also a Java version of LITE see CVS repository of