© STRL 1996-2008

| | | |||||||

| ## 5 Tools support
## 5.1 Project ObjectivesThe existing Tempura system is a simulator that tries to construct the sequence of states of the system corresponding to the specification. One drawback of the simulator is that it has only ASCII output. In addition, the correctness of systems is shown with help of ITL proof system [30, 14]. Experience with this proof system shows that a whole range of properties can be proven. However, these proofs are done ‘by hand’. For simple systems the proof task is still manageable but for complex systems, like the EP/3, it is nearly impossible.
## 5.2 Achievements
## 5.2.1 ITL proof checkerPVS 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 information. - The ITL library for PVS 2.1 patchlevel 2.417.
- The ITL library for PVS 2.2.
- The ITL library for PVS 2.3.
- The ITL library for PVS 2.4 patchlevel 1.
- The ITL library for PVS 3.2.
- Technical report.
Here is a sample proof of ITL: Proof: The following shows the same proof as a PVS session: - This is what we should prove:
RightChopImpChop :
|------- {1} (FORALL (f0: form, f1: form, f2: form): |-(f0 => f1) IMPLIES |-((f2 ^ f0) => (f2 ^ f1))) - With skolemization we eliminate the for-all quantifier.
Rule? (SKOSIMP)
Skolemizing and flattening, this simplifies to: RightChopImpChop : {-1} |-(f0!1 => f1!1) |------- {1} |-((f2!1 ^ f0!1) => (f2!1 ^ f1!1)) - Apply proof rule BoxGen.
Rule? (FORWARD-CHAIN "BoxGen")
Forward chaining on BoxGen, this simplifies to: RightChopImpChop : {-1} |-([](f0!1 => f1!1)) [-2] |-(f0!1 => f1!1) |------- [1] |-((f2!1 ^ f0!1) => (f2!1 ^ f1!1)) - Add an instance of lemma BoxChopImpChop. PVS will try to find the right instance.
Rule? (USE "BoxChopImpChop")
Using lemma BoxChopImpChop, this simplifies to: RightChopImpChop : {-1} |-([](f0!1 => f1!1) => (f2!1 ^ f0!1) => (f2!1 ^ f1!1)) [-2] |-([](f0!1 => f1!1)) [-3] |-(f0!1 => f1!1) |------- [1] |-((f2!1 ^ f0!1) => (f2!1 ^ f1!1)) - Apply proof rule MP.
Rule? (FORWARD-CHAIN "MP")
Forward chaining on MP, Q.E.D. Run time = 5.12 secs. Real time = 12.10 secs.
## Graphical interface for TempuraTempura, 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. - Version 2.10 (released 15-Oct-2002): gzipped tar file.
- Version 2.9 (released 31-Jan-2001): gzipped tar file.
The graphical interface of (Ana)Tempura is included in the source code and requires Tcl/Tk version 8.0 or higher 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. (Ana)Tempura can be compiled with the Gnu C compiler under a Unix like operating system like Sunos 4.1.3, Solaris 2.5.1 (and higher), Linux, cygwin etc. Contact: Email tempura@dmu.ac.uk 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.
Overview: Figure 2 shows an overview of AnaTempura. Figure 3 shows the interface of AnaTempura.
Figure 4 shows a graphical snapshot of a simulation of the ep/3 microprocessor specified in Tempura.
| | |||||||

| |