Formal modelling and verification of a component model using coloured petri nets and model checking
Elthon Allex da Silva Oliveira, Hyggo Oliveira de Almeida, Leandro Henrique Gomes da Silva · 2007
Component based software engineering has been claimed as a suitable approach to improve the flexibility and reuse in software development. In this context, the Compor infrastructure provides mechanisms to promote the dynamic composition of software systems, addressing applications with support for unanticipated requirement changes. In this paper, the formal modelling and verification of the COMPOR component model is presented. Hierarchical Colored Petri Nets are used for modelling and simulation, purposing to show the correct behavior for some scenarios. Model checking is used to prove that the scenarios analyzed with simulation are correct for all possible behaviors of the model.