Modeling Dynamic System Adaptation with Paradigm
- Day - Time: 14 October 2011, h.11:00
- Place: Area della Ricerca CNR di Pisa - Room: C-29
Speakers
- Erik de Vink (Eindhoven University of Technology & CWI Amsterdam, The Netherlands)
Referent
Abstract
Dynamic system evolution of cooperating software components can be modeled in the Paradigm language. Paradigm provides layers of granularity, allowing to describe component interaction at a higher level of abstraction. A special component called McPal gradually changes the interaction at the abstract level, guiding the dynamics of the system from the old AsIs situation into the new ToBe situation without the need for a system shutdown.
Paradigm models can be systematically translated into the process algebra mCRL2. An extensive toolset is available for mCRL2, including LTS visualization and symbolic model checking. Thus, exploiting this connection, tool-supported verification of system migration has become within reach. The approach is illustrated for a simple producer/consumer example. If time allows a demo of the use of mCRL2 is included in this talk.
Joint work with Luuk Groenewegen and Suzana Andova.