mCRL2 models, requirements and test logs for the EULYNX Point interface case study

mCRL2 models and mu-calculus formulas for the EULYNX Point Interface. Models and requirements are made in the context of the FormaSig project. Data is made available for replication purposes.

REQ_P_001, REQ_P_001_1 and REQ_P_002 are requirements for the point specific mCRL2 model point_spec.mcrl2

Remaining .mcf files are requirements for the generic PDI interface pdi_spec.mcrl2

Artifacts relating to testing are:

An mCRL2 model, mbt.mcrl2

A rename file to rename internal actions to tau, rename_file.re

Partial state space associated to mbt.mcrl2, partial_state_space.aut

The weak-trace bisim reduced version of the state space, partial_state_space_reduced.aut

Testing logs, test-logs.zip

The source code of the simulator and the testing tools, Simulator code.zip