Department of Computer Science

Square

Introduction

Simulation Verification (download)

The project file contains a manually generated semantics of the simulation for the Square example, as well as its correctness verification. The simulation was verified against the RoboChart model with assumptions TA1, TA2 and TA3.

The file with the CSP models and verification assertions is: src-gen/timed/square_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_MSquare [FD= PSimSpec
    assert PSimSpec [FD= PConstrainedSpecA3 \ ExternalEvents_MSquare
    

Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599