QUALITATIVE MODEL-BASED VERIFICATION OF OPERATING PROCEDURES BY HIGH-LEVEL PETRI NETS

The presence of colored tokens and time opens the possibility to combi ne high level Petri nets for describing operating procedures and const raint type qualitative models describing the model of the system over a wide operating range. Places can be associated to state variables an d the color of the tokens can be related to the qualitative value of t he variable. Are expressions correspond to qualitative model equations . A suitably modified version of the order of magnitude qualitative va lue representation form is used together with a scaling of each variab le to have the same uniform qualitative range. Operations are performe d on the interval arithmetic basis and only the result is transformed back to the uniform order of magnitude quantity space. This computatio n method ensures advantageous algebraic properties. Based on the above idea a novel verification method is proposed in this paper for testin g operating procedures against a qualitative model of the system using a high level or colored Petri net representation of the procedure and the model together.