PAT: Process Analysis Toolkit

An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems

Monthly archives for September, 2009

25, Sep, 2009: PAT supports user defined data structures


PAT only
supports integer, Boolean and
integer arrays for the purpose of efficient verification.
However, advanced data structures (e.g., stack, queue, hashtable and so
on) are necessary for some models. To support arbitary data structures, PAT
provides an interface to create user defined data type by inheriting an
abstract classes
ExpressionValue.

The
following is one simple example showing how to create a hashtable
in C#.


using System.Collections;
using
PAT.Common.Classes.Expressions.ExpressionClass;

//the namespace must be PAT.Lib, the class and method names can
be arbitrary
namespace PAT.Lib {
    public class
HashTable : ExpressionValue
{
        public Hashtable
table;

        /// Default
constructor without any parameter must be
implemented
        public HashTable()
{
           
table = new Hashtable();
       
}

        public
HashTable(Hashtable newTable)
{
           
table = newTable;
       
}

        public void Add(int
key, int value)
{
           
if(!table.ContainsKey(key))
{
               
table.Add(key,
value);
           
}
       
}
       

        public bool ContainsKey(int
key)
{
           
return
table.ContainsKey(key);
       
}

        public int
GetValue(int key)
{
           
return (int)table[key];
       
}

        /// Return the
string representation of the hash
table.
        /// This method must
be overriden
        public override
string ToString()
{
           
string returnString =
“”;
           
foreach (DictionaryEntry entry in table)
{
               
returnString += entry.Key + “=” + entry.Value +
“,”;
           
}

           
return returnString;
       
}

        /// Return a deep
clone of the hash table
        ///
This method must be
overriden
        public override
ExpressionValue GetClone()
{
           
return new HashTable(new
Hashtable(table));
       
}

        /// Return the
compact string representation of the hash
table.
        /// This method must
be overriden
        /// Smart
implementation of this method can reduce the state space and speedup
verification
        public
override string GetID()
{
           
string returnString =
“”;
           
foreach (DictionaryEntry entry in table)
{
               
returnString += entry.Key + “=” + entry.Value +
“,”;
           
}

           
return returnString;
       
}
   
}
}

 Note the
following requirements when you create your own data structure
objects:

  • The
    namespace must be “PAT.Lib”, otherwise it will not be recognized. There is no
    restriction for class names and method
    names.
  • Importing the PAT Expression name
    space using “
    using
    PAT.Common.Classes.Expressions.ExpressionClass;
    “.
  • Only
    public methods can be used in PAT models
  • The
    parameters must be of type “bool”, “int”, “int[]”  (int array) or object
    (object type allow user to pass user defined data type as
    parameter)
    .
  • The
    number of parameters can be 0 or many.
  • The
    return type must be of type “void”, “bool”, “int”, “int[]” (int
    array) or user defined data type
    .
  • The
    method names are case sensitive.
  • Put
    the compiled dlls in “Lib” folder of the PAT installation directory to make
    the linking easy by using #import
    “DLL_Name”;

if your
methods need to handle exceptional cases, you can throw PAT runtime
exceptions as illustrated as the following example.


public static int StackPeek(int[] array)
{
    if (array.Length >
0)
           return
array[array.Length – 1];

    //throw PAT Runtime
exception
    throw new
PAT.Common.Classes.Expressions.ExpressionClass.RuntimeException(“Access an
empty
stack!”);
}

To
import the libraries in your model, users can using following
syntax:

#import “PAT.Lib.Hashtable”; //to import a library under
Lib folder of PAT installation path

#import
“C:Program FilesIntelHashtable.dll”; //to import a library using absolute
path

To
declar the user defined types in your models, please use the following

syntax:

var<HashTable> table; //use the class name here
as the type of the varaible.

To
invoke the public methods in your models, please use the
following syntax
:

  • table.Add(10, 2);
  • if(table.ContainsKey(10))…


 


Copyright © 2007-2009 School of Computing, National University of
Singapore

05, Sep, 2009: PAT 2.7.0 is released!

What’s new in PAT 2.7.0

In this release, the main achievement is that timed refinement checking algorithm is implemented in Real-Time System (RTS) module. At this stage, all the planned algorithms are implemented in RTS module. In the future, we will work on the syntax enrichment and performance improvement for RTS module. In this release, modeling languages in CSP and RTS modules are improved for better expressiveness power and parsing precision. Other updates include new examples and bug fixing.

Timed Refinement
Sometimes timing aspects are important in the system requirment, e.g., human heart must beat at rate between 50/minute to 200/minute (too low or too high is vital for human lifes). In these cases, we can use time refinement to check whether the input model follows the desired timing requirement. The syntax is the following:

#assert Implementation() refines< T> TimedSpec() ;

Note: For timed refinement checking, RTS module uses a timed trace semantics (i.e. a mapping from a model to a set of finite timed event sequences) and a timed trace refinement relationship (i.e. a model satisfies a specification if and only if the timed traces of the models are a subset of those of the specification). The verification algorithm developed for timed refinement checking will verify that a system model is consistent with a specification by showing a refinement relationship. A timed event sequence is presented as a counterexample if there is no such refinement relationship. For the timed refinement checking, PAT requires that the implementation or specifications are not divergent, otherwise the shared clock will not be bounded. If the system is divergent, PAT will ask user to provide a ceiling for the shared clock (default is 2^15).

Process Parameters are Supported in Grouped Processes
In order to have better compositional behaviors, we allow process parameters to be used in in grouped processes. For example, in []x:{0..n}@P or ||| {0} @ P() , n can be a global constant or process parameter, but not a global variable. We make this restriction for the performance reason. For example, the following definitions are all valid in PAT.
#define n 10; |||x:{0..n}@P;
P(n) = |||x:{0..n}@Q;

Channel Names can be Used as Event Names
Event name is an arbitrary string of form (‘a’..’z’|’A’..’Z’|’_’) (‘a’..’z’|’A’..’Z’|’0′..’9’|’_’)*. However, global variable names, global constant names, process names, process parameter names, propositions names can not be used as event name. One exception is the channel names are allowed, because we may want to use channel name in specification process to simulate the channel behaviors and use refinement checking to compare with real channel events.

Divergence-free
Given P() as a process, the following assertion asks whether P() is divergence-free or not.
#assert P() divergencefree;
Given a process, it may performs internal transitions forever without engaging any useful events, e.g., P = (a -> P) {a};, In this case, P is said to be divergent. Divergent system is ususally undesirable.

Timed Divergence-free
Given P() as a process, the following assertion asks whether P() is timed divergence-free or not.
#assert P() divergencefree< T>;
Given a process, it may performs internal transitions and timed transitions forever without engaging any useful events, e.g., Q = (a -> Wait[5]; Q) {a};, In this case, P is said to be timed divergent. Timed divergent system is undesirable, which can give unbounded timer, which disallows timed refinement checking.

Note: P = (a -> P) {a}; is divergent, but not timed divergent, because it performs internal transitions forever without timed transitions.

Others
1 User manual is updated to latest implementation.
2 Real-Time system examples (Timed PaceMaker) and timed refinement assertions are added.
3 Fix the bugs in parsing, GUI and other places.