You are here

Modelchecking evolution on-the-fly

18 January 2012
Ex Boccherini - Piazza S. Ponziano 6 (Conference Room )
The coordination modeling language Paradigm distinguishes fine-grained behaviour of transitions between states and coarse-grained behaviour of transfers between phases in component-based systems. The semantics guarantees vertical consistency of states and phases within a component. Protocols maintain horizontal consistency for collaborations of components. By adapting the protocols at run-time, system evolution can be arranged on-the-fly. We discuss for examples of a critical-section problem and a production line how dynamic system adaptation using the symbolic model checker mCRL2 can be verified
De Vink, Erik