Specification and Verification of Real-Time Constraints in Coarse-Grain Dataflow
MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE
Pagination or Media Count:
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 programs timing, the user specifies all possible behaviors of each dataflow module and assigns timing costs to each modules 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.
- Computer Programming and Software