Current Petri net based methods for modeling and design of real-time systems rely on formalisms that are either expressive or analyzable, but not both. Our goal is to provide a new formalism bridging the gap between these positions. We start from a well known result on timed marked graphs, extend it to more general nets, and enhance the resulting formalism expressiveness by means of a set of transition expansion rules, which also enable hierarchical net structuring. A detailed example is discussed.>

Abstract The PROTOB object‐oriented methodology for the executable specification of large‐scale event‐driven systems is introduced and described. Two supporting features of PROTOB are also presented: the graphic and textual language that formally describes the behaviour of objects, which is based on high‐level Petri nets called “PROT nets” and which is demonstrated to be more powerful than SA/RT dataflows; and a CASE environment with tools for specification, modelling, simulation and prototyping. Use of PROTOB is illustrated by discussion of the automated generation of distributed systems running on a network of VMS and UNIX computers.