Technical Report Number
Theory of Computation, Data, Computer Systems Organization
While traditional Data Flow Diagrams (DFDs) are popular, they lack the formality needed in a good specification technique. We provide an executable semantics for a subset of RT-SPECS, a formalization of DFDs, using the programming language Standard ML. RT-SPECS is a formal notation for specifying concurrent and real-time software that relies on model-based specification of abstract datatypes. Processes are specified using assertions rather than algorithms. Because our semantics of RT-SPECS is written in SML, it is also an interpreter, yielding a directly executable specification language.