SimFW

Introduction

Simulation Verification (download)

This project archive contains a manually generated semantics of the simulation for the SimFW example, as well as its correctness verification, and the exploration of several simulation variations with intentional design mistakes, which are automatically detected by our verification strategy.

The simulation (and its variations) were verified against the RoboChart model with assumptions TA1, TA2 and TA3.

The file with the CSP models and verification assertions is: src-gen/timed/SimFW_assertions-noabstracteventsinthesemantics.csp

The interested reader can load this file in the FDR4 tool and check the assertions. The relevant assertions are:

• Absence of deadlock below indicates that the RoboChart model is schedulable.

  assert PConstrainedSpecA3; TSTOP :[deadlock free]
  

• The assertions below ensure that the RoboSim model is equivalent to the RoboChart one with the assumptions.

  assert PConstrainedSpecA3 \ ExternalEvents_CFootBot  [FD= SimSpec
  assert SimSpec [FD= PConstrainedSpecA3 \ ExternalEvents_CFootBot
  

  There are similar assertions that uncover the problems with mistaken simulations.

Simulation Verification (download)

The project archive contains the generated semantics of the simulation for the SimFW example, as well as its correctness verification.

This semantics was verified against a manually defined semantics for the same example. This manually defined semantics was proven correct against the RoboChart model with assumptions TA1, TA2 and TA3.

By transitivity, the generated semantics is, therefore, a correct implementation of the RoboChart model with the assumptions.

The file with the CSP models and verification assertions is: src-gen/timed/SimFW-semanticsVerification.csp

The interested reader can load this file in the FDR4 tool and check the assertions. The relevant assertions are:

assert SimSMovement [FD= SimSpec
assert SimSpec [FD= SimSMovement

assert SimSMovement [FD= SimCFootBot
assert SimCFootBot [FD= SimSMovement

The first two assert that the simulation machine generated (SimSMovement) has the same behaviour (in the Failures-Divergences model of CSP) as the manually defined simulation machine (SimSpec).

The latter two assertions ensure that, for this example, the module SimCFootBot behaves the same as the generated simulation machine, since the module has a single controller that, itself, has a single machine.