Specification and Verification of Real-Time Constraints in Coarse-Grain Dataflow
Dana S. Henry · 1991
Abstract : We present a method for verifying real time constraints in a distributed, coarse-grain dataflow environment starting with a program which has already been allocated onto a machine. The user specifies the timing of each module together with real-time constraints; and we verify the constraints. To deduce program's timing, the user specifies all possible behaviors of each dataflow module and assigns timing costs to each module's behavior. We use the behavior and timing of individual modules to derive a data independent timing model for the entire program. User specifiable constraints include conditional constraints and constraints through non-deterministic paths. An event-driven verification verifies constraints. We justify the need for an event-driven verification, describe design issues, and offer a tagging scheme for sharing state among multiple verifications.