Ruud Meeuws: Model Checking Supermodels Workbench with mCRL2

Event Details

At Sioux, a model-driven development tool is created. It allows users to create a model and generate software for specific hardware platforms. For this tool, Sioux wants to incorporate model checking in order to improve the correctness and safety of software. To see whether model checking is viable for industrial models, we want to explore the possibilities in limiting behaviour such that model checking becomes feasible. We specify several execution models and see the influence of
them on the efficiency and feasibility of model checking with mCRL2 for this development tool.