Testing and Verification


The Liège Automata-based Symbolic Handler (LASH)

LASH is a toolset developed at the University of Liège for representing infinite sets and exploring infinite state spaces. It is based on finite-state representations, which rely on finite-state automata for representing and manipulating infinite sets of values over various data domains.
The current version of LASH is beta version 0.92 and consists of:

C libraries providing functions and datatypes for performing the following tasks:
  • Constructing and manipulating some types of finite-state automata (on finite and infinite words).
  • Representing and manipulating finite and infinite sets of values. The representation systems implemented by LASH are:
    - The NDD (Number Decision Diagram), suited for sets of unbounded integer vectors. NDDs are slightly more expressive than Presburger arithmetic.
    - The RVA (Real Vector Automaton), suited for sets of unbounded real and integer vectors. RVA can represent all the sets that can be defined in the first-order combined additive theory of the reals and integers.
    - The QDD (Queue-content Decision Diagram), suited for sets of contents of unbounded FIFO queues.
  • Exploring the state-space of systems composed of a finite control and of unbounded integer variables over which linear operations are performed.
  • Front-ends for:
    - Compiling program models expressed in the Simple-PROMELA and the Simple-IF languages, and exploring the state-space of these programs.
    - Solving problems expressed in Presburger arithmetic.
    The following features are under development and will soon become part
    of the toolset:
  • State-space exploration tools for timed systems and hybrid systems, based on the RVA package.
  • A visualization tool for sets represented by NDDs and RVA.

More information on LASH

(c) Artist Consortium, All Rights Reserved - 2006, 2007, 2008, 2009

Réalisation Axome - Création de sites Internet