kpWorkbench

About

kpWorkbench is a software framework which facilitates the simulation and formal verification of Kernel P systems via the SPIN model checker. kpWorkbench aggregates a set of tools which process a kP system model, expressed in kp-lingua, translates it to a Promela specification and mediates the SPIN based simulation and model checking.

The framework is implemented in C# and requires Microsot's .NET platform (or Mono on UNIX machines) to run.

Download

kpWorkbench is freely distributed under the GPL license. We are currently in the early stages of its development and consequently, we cannot guarantee stability and soundness of behaviour at this particular point. We also highlight the fact that kpWorkbench supports Kernel P system models only and is not compatible with any other variants.

Requirements

Download kpWorkbench

Run

kpw <file>.kpl [<n> steps];

The default action when a kpl file is supplied is to simulate the kP system contained n number of steps (n defaults to 20 if a value is not specified).


kpw simulate <file> [<n> steps];

For the purpose of clarity one may explicitly include the "simulate" keyword, which also instructs kpWorkbench to treat the input file as a kp-lingua specification even if it does not have the .kpl extension.


kpw <file>.kpx;

Loads a kpx file, which presents a Kernel P system experiment. More details on this form of input and the structure and content of a kpx file will follow shortly.