Summary
Embedded devices often run both critical safety functions and less important ones, and making sure these safety functions work correctly depends on how they are arranged and scheduled on the device’s processor cores. The authors present SafeDSE, a tool that helps decide how to organize, place, and schedule safety features in dataflow applications to meet performance and safety requirements together. Their approach checks and proves that the chosen setup is safe using formal arguments, and it finds better solutions than simpler methods that decide some parts separately. This extended work shows the entire system, proves it can find optimal solutions for small cases, and discusses tests and challenges they faced.
What this means in practice
- •For embedded systems engineers: Automatically find schedules and safety configurations that meet throughput and safety requirements for mixed-criticality streaming functions on embedded platforms.
- •For automotive software teams: Generate verifiable safety arguments and optimal deployment plans for streaming dataflow applications with varying safety criticality levels in vehicles.
Abstract
Embedded platforms increasingly host safety-related streaming functions next to less critical ones. Whether a safety architecture pattern, such as a doer/checker pair, protects a function depends on the cores that run its components. Their schedule must meet the throughput requirement, and mixing safety integrity levels (SILs) on one core raises development cost. This report presents SafeDSE, a design space exploration framework for synchronous dataflow applications. One declarative constraint model decides the pattern of each actor, the placement that the fault model requires, the static-order schedule, and the platform, and prices SIL promotion. Guards activate the chosen patterns in a fixed graph that holds all of them, and node potentials encode throughput. An independent verifier re-checks every solution, and a generator turns its checks into evidence of a safety argument in Goal Structuring Notation. On 9 benchmark instances under period bounds, no rule that fixes patterns before mapping was both always feasible and never more expensive under conservative pricing, while joint exploration was. In the generated arguments, 49 to 62% of the leaves cite verifier checks; the rest are claims a mapping cannot discharge. Optimality within the model was proven for all synthetic graphs with up to 16 actors. This extended version adds the full model, the verifier and generator in detail, the complete catalog and parameters, and a proof of the potential characterization. It also reports every experiment per instance, a mutation analysis of the verifier, and the negative results of the development.