A FORMAL APPROACH TO MODELLING OF REAL-TIME SYSTEMS USING RTCP-NETS

摘要

The paper deals with an application of formal methods for modelling of real-time systems. The main objective of this approach is to support development of these systems in order to ensure that the produced software artefacts are correct, as well as to improve the development process. The Real-Time Coloured Petri nets (RTCP-nets), which are a subclass of time coloured Petri nets, are used as a modelling tool. To make the nets more suitable for modelling and analysis RTCP-nets are derived from coloured Petri nets. Applications of RTCP-nets as a modelling and verification tool are strongly supported by the so-called Adder Tools. The formal description of RTCP-nets is not presented here since the paper focuses on the main properties of these and the supporting facilities of the Adder Tools. The approach is illustrated by a practical example, that shows the expressiveness of RTCP-nets for modelling and verification of real-time systems.