Coloured Petri nets and graphical animation: a proposal for a means to address problem frame concerns
Jens Bæk Jørgensen · Expert Systems · 2008
Abstract: To address a frame concern in Jackson's problem frames, we must make appropriate descriptions of (1) the problem domain; (2) the requirements; (3) the specification of the machine. Based on these descriptions, we must give a convincing argument that the given domain properties and the machine specification together entail that the requirements are fulfilled. In this paper, we demonstrate how to address certain frame concerns with the use of the formal modelling language coloured Petri nets (CPN). Problem domain description and machine specification are brought together in a CPN model, which is augmented with a graphical animation. The CPN model is executable and we simulate it to address frame concerns. We illustrate the approach on the elevator controller example.