GIVING SEMANTICS TO SA/RT BY MEANS OF HIGH-LEVEL TIMED PETRI NETS

In the IPTES project a dual language approach is proposed for overcoming both the problems derived from the use of a user-friendly, high-level, but not-formally-defined language and from a lower-level, formal, but difficult-to-use language. The approach uses a user-friendly, high-level language as user interface and a lower-level, formal language as machine language. In this way the users can both access the IPTES environment through a nice interface and can profit from non-ambiguity-checks and proofs algorithms based on the formal kernel machine language. The correspondence between the two languages is built-in in the IPTES environment that provides a transparent mapping mechanism that relates the users specifications expressed by means of the high-level interface language with the for-mal definitions expressed in the formal machine language. This paper presents the mapping mechanism that relates the current IPTES user interface (SA/RT (Ward and Mellor 1985)) with the IPTES machine language (high-level timed Petri nets (Ghezzi, Mandrioli, Morasca and Pezze 1991)). As a side effect, it also presents the formal semantics of SA/RT defined by means of high-level timed Petri nets.