STRL STRL
© STRL 1996-2008







5 Tools support

5.1 Project Objectives

The 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 [3014]. 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 checker

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 information.

Here is a sample proof of ITL:

RightChopImpChop    ⊢  f0 ⊃  f1  ⇒   ⊢  f2;f0 ⊃  f2;f1

Proof:

1  f0 ⊃  f1                         given
2  !(f0 ⊃  f1)                      BoxGen
3  !(f0 ⊃  f1) ⊃  (f2;f0) ⊃  (f2;f1) BoxChopImpChop
4  f2;f0 ⊃  f2;f1                   2,3,MP

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 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:

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.

Publications:

Overview: Figure 2 shows an overview of AnaTempura.



Figure 2: Overview of AnaTempura

Figure 3 shows the interface of AnaTempura.



Figure 3: Interface of AnaTempura


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



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








Aug 18 2011
Home | Training | Research | People | About | News