Denotational Semantics of a Real-Time Prototyping Language

摘要

The denotational semantics of the Prototype System Description Language PSDLis formally described in terms of an algebra-based Petri net model in this paper. PSDLsupports specification and design of software prototypes that have to satisfy hard realtime constraints. The language is derived from a dataflow model that is augmentedby data abstraction facilities and application-oriented timing and control constraints.In the Petri net model, each net is associated with a many-sorted partial algebraand is labeled with terms and marked with data of that algebra. The algebra servesto interpret the built-in and user-defined data types and functions of a specification,while the net defines a partial order semantics of its dynamic behavior. To capturethe semantics of timing constraints in PSDL we constrain transitions by conditionsdepending on time values of abstract clocks modeling the local time of distributedcomputational resources.