Formal Verification
The sdf3verify-sadf tool allows formal verification of some properties of the structure and behaviour of SADF graphs. Next to checking several basic properties, it allows to determine whether an SADF graph could be captured with a less expressive model of computation such that it actually resembles for example an HSDF, SDF or CSDF graph.
Basic Properties
| Tools | sdf3verify-sadf --check connected_graph sdf3verify-sadf --check is_timed sdf3verify-sadf --check ergodicity sdf3verify-sadf --check strong_consistency sdf3verify-sadf --check simple_sdf_collection |
APIs | SADF_Verify_SingleComponent() SADF_Verify_Timed() SADF_Verify_SimpleErgodicity() SADF_Verify_StrongConsistency() SADF_Verify_SimpleStronglyConsistentSDFCollection |
|---|---|
These features allow verifying respectively the following basic properties:
| Property | Definition |
|---|---|
| Connected SADF Graph | Defines that an SADF graph consists of a single connected component |
| Timed SADF Graph | Defines that an SADF graph includes a process with a positive execution time in some scenario |
| Ergodic SADF Graph | Defines that the timed probabilistic system implied by the semantics of an SADF graph includes exactly one terminating strongly connected component. This matches with the traditional definition of ergodicity for Markov chains |
| Strongly Consistent SADF Graph | Strong consistency of an SADF graph is a structural property which specifies that for each possible subscenario combination of the included detectors, the structure of the resulting SADF graph resembles the structure of a consistent SDF graph in such a way that all detectors have a repetition vector entry equal to 1. The current algorithm can only decide on strong consistency for SADF graphs with no more that 1 Detector. |
| Simple SDF Collection | Stronly consistent SADF graphs with at most one detector such that the execution times for all (sub)scenarios are fixed can be abstracted into an FSM-based SADF graph. Such SADF graphs basically represent a simple collection of consistent SDF graphs, one for each scenario in which the SADF graph can operate. |
Models of Computation
| Tools | sdf3verify-sadf --check is_hsdf sdf3verify-sadf --check is_sdf sdf3verify-sadf --check is_csdf sdf3verify-sadf --check moc |
APIs | SADF_Verify_HSDF() SADF_Verify_SDF() SADF_Verify_CSDF() SADF_Determine_MoC() |
|---|---|
SADF generalises other dataflow models as follows:
| Dataflow Model | Definition |
|---|---|
| CSDF Graph | An SADF graph for which the execution time distribution for all scenarios of all processes are actually point distributions and for which each Markov chain associated with all detectors represents a deterministic cycle (using probabilities of 1 only) that lacks transient states. Initial control tokens that might be available and hierarchical control relations should not imply any behaviour that is different from cyclo-static behaviour. The current algorithm disallows hierarchical control and initial control tokens to be presence in an SADF graph that resembles a CSDF graph. |
| SDF Graph | An SADF graph with only kernels (operating in a default scenario) for which the execution time distribution are actually point distributions |
| HSDF Graph | An SADF graph with only kernels (operating in a default scenario) for which the execution time distribution are actually point distributions and with all production and consumption rates equal to 1 |