High-Level Timed Petri Nets as a kernel for executable specifications

One of the goals of the IPTES environment is to provide a highly usable and formally based specification support environment for real-time applications. Therefore the environment is built upon a formal language that provides a sound, and mathematically well-defined kernel for IPTES. The language provides a means for formulating unambiguous specifications that can be formally verified at any stage of the project. The ability of verifying the specifications from the early stages of the project is very important for revealing errors when their correction can be done at a much lower cost compared with the cost of removing the same errors in later phases.The formal kernel of IPTES is a class of high-level Petri nets, called HLTPNs (High-Level Timed Petri Nets), that allow specifications to be executed, simulated, tested and formally proved.HLTPNs come in two forms: the internal form (HLTPN _i ) and the abstract form (HLTPN _a ).HLTPN _i may be viewed as the machine language of the abstract machine underlying the IPTES environment.HLTPN _a provides a higher-level intermediate notation that allows to deal explicitly with aspects related to scheduling of the modeled system.This material is based upon work supported by the esprit project IPTES and by CNR—Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo.