Oct 02, 2012: Ferry Olthuis and Daan van Beek: DVL: Action weaving for improving verification performance of large mCRL2 models

October 02, 2012DVL: Action weaving for improving verification performance of large mCRL2 models
Room: Zi 5126Ferry Olthuis and Daan van Beek
12:30-13:30

This talk introduces some new methods to do verification of large mCRL2 models. We introduce a language extension called DVL, which inserts new actions into the model that are used for verification. We use this DVL construct in combination with an extra process (monitor) and in combination with the traditional mu calculus approach. We show how we can verify larger models with this approach.

We also introduce  implementation based modeling in which we use an old implementation to verify the model for a new implementation which in turn can be used to verify the new implementation. The reliability from the old implementation is transferred to the new implementation using the improved model.