Synchrone

Overview

This plug-in extracts a synchronous-reactive model from a reactive program written in C. The extracted model is encoded in Lustre and can be extended with user-specified safety properties expressed as Lustre synchronous observers. Synchronous model-checkers, including GATeL and Kind2, can then be used to verify these properties.

Usage

Consider the following typical reactive program:

int main(void) {
  init(); /* initialize some global state */

  while (synchronize()) {
    read_inputs();

    /* compute new outputs based on the internal state and the inputs */
    cycle();

    write_outputs();
  }
}

As the function cycle is executed repeatedly within a main loop, with new inputs at each iteration, this program follows a reactive execution model. By analyzing the behavior of init and cycle, the Synchrone plug-in can extract a Lustre synchronous model in which each iteration of the outer loop corresponds to one logical instant.

Running Synchrone with

frama-c -sync -sync-init init -sync-cycle cycle cycle.c

extracts a semantically equivalent synchronous model in Lustre. For example, if cycle has a boolean input reset and an integer output y (specified using dedicated ACSL annotations), the extracted model may look as follows:

node Cycle(reset: bool) returns (y: int);
let
  (* equations *)
tel

Additionally, the plug-in can also link user-specified observers to the extracted model using:

frama-c -sync -sync-init init -sync-cycle cycle cycle.c observer.lus

where observer.lus contains the synchronous observers. For instance, to express that the output y is increasing whenever reset is false, one can write the following contract:

node Cycle(reset: bool) returns (y: int);
  behavior {
    assumes H1 { not reset };
    ensures P1 { true -> y > pre(y) };
  }

The resulting model can then be given directly to Kind2 or GATeL for verification.