Symbolic Analysis Laboratory (SAL)

SAL is a project established by Berkeley and Standford Universities used for automated formal methods.

Motivation for SAL is the following (the link):

To become practical for assurance, automated formal methods must be made more scalable, automatic, and cost-effective. Such an increase in scope, scale, automation, and utility can be derived from an emphasis on a systematic separation of concerns during verification. SAL (Symbolic Analysis Laboratory) attempts to address these issues. It is a framework for combining different tools to calculate properties of concurrent systems.

SAL defines symbolis analysis as follows:

Symbolic analysis is simply the computation of fixed point properties of programs through a combination of deductive and explorative techniques.
SAL sees the key elements of symbolic analysis as

  1. Automated deduction, in computing property preserving abstractio9ns and propagating the consequences of known properties.
  2. Model checking, as a means of computing global properties of by means od systematic symbolic exploration. For this purpose, model checking is used for actually computing fixed points such as the reachable state set, in addition to verifying given temporal properties.
  3. Invariant generation, as a technique for computing useful properties and propagating known properties.
  4. SAL 3.0  is the current the tool suite for SAL SAL tutorial can be downloaded from here: http://sal.csl.sri.com/doc/salenv_tutorial.pdf

Principles of SAL 3.0

The “motor” of SAL is its language.

The SAL language is not that different from the input languages used by various other verification tools such as SMV, Murphi, Mocha, and SPIN. Like these languages, SAL describes transition systems in terms of initialization and transition commands. These can be given by variable-wise definitions in the style of SMV or as guarded commands in the style of Murphi.

A complete description of the SAL language is available online at http://sal.csl.sri.com/.

Simple example using SAL:
short: CONTEXT = 1
BEGIN
  State: TYPE = {ready, busy};
  main: MODULE =
  BEGIN
    INPUT request : BOOLEAN
    OUTPUT state : State
    INITIALIZATION
    state = ready
    TRANSITION
    state’ IN IF (state = ready) AND request THEN
      {busy}
     ELSE
      {ready, busy}
     ENDIF
  END;
END
Starting the program happens as follows:   sal > (start-simulation! “main”)

Some observations considering reverse engineering and program comprehension (Laitila’s approach):
  1. SALenv contains a symbolic model checker called sal-smc.  It allows users to specify properties in linear temporal logic (LTL), and computation tree logic (CTL). One typical command for sal-smc is:  THEOREM main |- AG(request => AF(state = busy));
  2. Some other featrures are Peterson protocol, Bakery protocol and Syncronous bus arbiter etc. Some examples.

Some comments:

  1. That kind of language specific approach leads to a procedural paradigm via a program which indirectly describes the model.  In that approach the model to be verified is data, which tries to model the code.
  2. The implementation language SAL 3.0 is very far from the programming languages. Therefore, SAL is not useful for reverse engineering or for program comprehension.

Some links:

Advertisements