SafeDSE: Joint Exploration of Safety Architecture Patterns, Mapping, and Scheduling for Dataflow Applications With Safety Arguments (Extended Version)

Fatemeh Bahrami; Seyed-Hosein Attarzadeh-Niaki

cs.AROct 12, 2026

SafeDSE: Joint Exploration of Safety Architecture Patterns, Mapping, and Scheduling for Dataflow Applications With Safety Arguments (Extended Version)

Authors: Fatemeh Bahrami, Seyed-Hosein Attarzadeh-Niaki

Organizations: Faculty of Computer Science and Engineering, Shahid Beheshti University, Tehran, Iran

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.

Figures & tables

Fig. 1: SafeDSE design flow. The front-end turns all design alternatives into one fixed constraint instance; the model decides and proves the optimum within the model. Only checks of an independent verifier, which shares no code with the model, become evidence in the generated argument; dashed arrows are rejections and refusals.

Approach	Thr.	Exact	Pat.	Place.	Cost	Arg.
DeSyDe [ 28 , 7 ]	✓	✓	✗	✗	✗	✗
Bonfietti et al. [ 27 , 5 ]	✓	✓	✗	✗	✗	✗
Jordão et al. [ 8 ]	$\circ$	✓	✗	✗	✗	✗
Kang et al. [ 16 ]	$\circ$	✗	$\circ$	$\circ$	✗	✗
Tămaş-Selicean, Pop [ 12 ]	$\circ$	✗	$\circ$	✗	✓	✗
Parker et al. [ 13 ]	✗	✗	$\circ$	✗	✓	✗

TABLE I: Comparison With Related Work

Platform file	Card	Core type	Cores	Max.	Card price	Modes (cycle factor, core price)	$\mathit{SIL}^{\max}$	Part.	Memory
mixed.xml	R-card	cortexR	2	3	120	standard (1, 40); eco (1.3, 40)	4	yes, 15	64000
	M-card	cortexM	4	4	25	standard (1.6, 8); performance (1.2, 11)	2	no	16000
mixed_noiso.xml	R-card	cortexR	2	3	120	standard (1, 40); eco (1.3, 40)	4	no	64000
	M-card	cortexM	4	4	25	standard (1.6, 8); performance (1.2, 11)	2	no	16000
mixed_3type.xml	R-card	cortexR	2	3	120	standard (1, 40); eco (1.3, 40)	4	no	64000
	P-card	ppcE200	2	3	140	standard (1.15, 45)	4	no	48000

TABLE II: Card Templates of the Platforms in the Evaluation

Panel of Figure 4 — Fig. 2: (a) Running example: RASTA speech front end with the required SIL of each actor (badge), and the FCR templates of the platform. (b) Four catalog patterns with their placement relations (white: owner, shaded: added component, dot: initial token). Both doer/checker patterns have the same structure and differ only in placement, which the fault model selects; the evaluation instances use subsets of the catalog.

Pattern	Adds	Placement per fault class	SIL	Covers
none	–	–	0–1	–
Low-SIL D/C	$c$	H: $o\neq_{c}c$	1–2	H
Same-CPU D/C	$c$	$o=c$	1–2	S
2-of-2	$b$	H: $o\neq_{f}b$ ; S: $o\neq_{t}b$	3–4	H, S
High-SIL isolated D/C	$c$	H: $o\neq_{f}c$	3	H
Mixed-SIL D/C	$c_{1},c_{2}$	H: $o\neq_{f}c_{1}$ , $c_{1}\neq_{f}c_{2}$ ; S: $c_{1}\neq_{t}c_{2}$	3–4	H, S

TABLE III: Pattern Catalog (Excerpt of the Data File)

Profile	SIL 0	1	2	3	4
Myklebust et al.	1.00	1.13	2.25	5.18	9.06
Klosterman	1.00	1.13	1.23	1.70	2.35
Klosterman (lower row)	1.00	1.13	1.23	1.40	1.59
DO-178B	1.00	2.00	3.00	5.00	9.00

TABLE IV: Development-Cost Profiles

Pattern	Components (WCET, $\Delta$ SIL)	Edges (tokens)	Inputs to / output from	Failure	Rec.	Mult.	Tactics
none	–	–	– / –	none	0	–	–
Low-SIL D/C	$c$ (checker, $-1$ )	$o\!\to\!c$ (0), $c\!\to\!o$ (1)	$c$ / $o$	active	2	1	SaC, RR
Same-CPU D/C	$c$ (checker, $-1$ )	$o\!\to\!c$ (0), $c\!\to\!o$ (1)	$c$ / $o$	active	1	1	SaC
2-of-2	$b$ (full, 0)	$o\!\to\!b$ (0), $b\!\to\!o$ (1)	$b$ / $o$	silent	2	1 (2 d )	RR, Cmp, Vot, DR
High-SIL isolated D/C	$c$ (checker, 0)	$o\!\to\!c$ (0), $c\!\to\!o$ (1)	$c$ / $o$	silent	2	1	SaC, RR
Mixed-SIL D/C	$c_{1}$ (checker, $-2$ ), $c_{2}$ (checker, $-2$ )	$o\!\to\!c_{1}$ (0), $o\!\to\!c_{2}$ (0), $c_{1}\!\to\!c_{2}$ (1), $c_{2}\!\to\!c_{1}$ (1), $c_{1}\!\to\!o$ (1)	$c_{1},c_{2}$ / $o$	silent	3	1	SaC, Cmp, RR, Vot, DR

TABLE V: Pattern Catalog: Structure and Attributes of Every Record

Pattern	Scen.	Covers	Tactics	General scenario (catalog text)
Low-SIL D/C	SC1	–	Sanity Check	An implausible output of the doer is detected by the checker.
	SC2	H	Replication Redundancy	A random hardware fault in the doer’s processor does not prevent detection, because the checker runs on another processor.
Same-CPU D/C	SC1	–	Sanity Check	An implausible output of the doer is detected by the checker.
2-of-2	SC1	–	Comparison	A fault in either channel is detected as a disagreement between the two channels.
	SC2	H	Replication Redundancy	A random hardware fault in one channel does not affect the other channel.
	SC3	S	Diverse Redundancy	A systematic fault is not common to both channels.

TABLE VI: General Scenarios of the Catalog Patterns

Panel of Figure 9 — Fig. 3: (a) Guarded superposition of compJah under both fault classes: each slot is guarded by the patterns that use it, the graph is fixed, and only $\mathit{pat}$ is a variable. (b) MSAG of a two-core binding of the running example, with one remote channel refined for the TDMA bus. Not drawn: the one-token self-edge of every actor and the refinement of the other remote channels.

Fig. 4: Excerpt of the argument generated for a verified optimum of the running example under both fault classes: actor backEnd (SIL 2, low-SIL diverse doer/checker), ids as generated, texts shortened. Deployment goals claim exactly what their log records establish; the remaining common causes and the method goals (diamonds) stay with the engineer. The method goal is drawn once.

Fig. 5: Second excerpt of the same argument: actor compJah (SIL 3, 2-of-2). The replication goal cites the DIFFERENT_FCR record and the diversity goal the DIVERSE record of the same pair; Comparison and Voting are value-domain tactics and stay undeveloped. Generated by the script of Fig. 4 .

Tactic	Category	IEC 61508-7 methods	Relations	Patterns using it
Sanity Check	Checking	A.1.2 monitoring relay contacts; A.2.7 analog signal monitoring; A.3.1-A.3.3 self-tests; A.4.1-A.4.4 checksums; A.5.1-A.5.5 RAM tests; A.6.1 test pattern; A.9 temporal and logical program monitoring; C.3.3 assertion programming; C.5.3 interface checking	–	Low-SIL D/C, Same-CPU D/C, High-SIL isolated D/C, Mixed-SIL D/C, Low-SIL diverse D/C
Condition Monitoring	Checking	A.1.1 failure detection by online monitoring; A.6.4 monitored outputs; A.9 temporal and logical program monitoring; A.13.1 monitoring	–	–
Comparison	Checking	A.1.3 comparator; A.6.5 input comparison/voting	–	2-of-2, Mixed-SIL D/C, Dual 2-of-2, 3-version (NVP)
Replication Redundancy	Redundancy	A.2.1 tests by redundant hardware; A.2.5 monitored redundancy; A.3.5 reciprocal comparison by software; A.4.5 block replication; A.6.3 multi-channel output; A.7.3 complete hardware redundancy; A.7.5 transmission redundancy	DIFFERENT_FCR , DIFFERENT	Low-SIL D/C, 2-of-2, High-SIL isolated D/C, Mixed-SIL D/C, Dual 2-of-2, 1-of-2 failover, Low-SIL diverse D/C, 3-version (NVP)
Diverse Redundancy	Redundancy	A.7.6 information redundancy; A.13.2 cross-monitoring of multiple actuators; B.1.4 diverse hardware; C.4.4 diverse programming	DIVERSE	2-of-2, Mixed-SIL D/C, Low-SIL diverse D/C, 3-version (NVP)
Voting	Masking	A.1.4 voter; A.6.5 input comparison/voting	–	2-of-2, Mixed-SIL D/C, Dual 2-of-2, 3-version (NVP)

TABLE VII: Tactic Table: Tactics, IEC 61508-7 Methods, and Deployment Relations

Instance	Platform	FM	$\|G^{+}\|$	Vars	Cost	Cores	$\mu^{*}$	$t$ (s)
p_rasta	2T, part.	H	26	11k	3330	2	235	6.0
f_random_hw	2T	H	26	11k	3349	5	235	8.7
d_random_hw a	2T	H	18	7k	1857	3	235	6.0
d_systematic_sw a	2T	S	14	5k	1846	2	235	3.3
f_sw3	3T	S	18	8k	3365	4	235	5.2
f_both3	3T	H+S	18	8k	3406	5	235	3.2

TABLE VIII: Pattern Instances and Joint Optima (All Solutions Verified)

Instance	Front-end	Solve	Period step	Verifier	Generator
p_rasta	0.14	6.2	0.53	0.09	0.17
f_random_hw	0.14	9.5	0.55	0.09	0.17
d_random_hw	0.16	7.1	0.56	0.10	0.17
d_systematic_sw	0.15	3.5	0.50	0.10	0.17
f_sw3	0.14	5.7	0.46	0.08	0.15
f_both3	0.14	3.4	0.48	0.10	0.16

TABLE IX: Time per Pipeline Stage (s)

Scenario	$\mu$	$t$	$\mu$	$t$	pr.	$\mu$	$t$
	Article		DeSyDe here			SafeDSE
3: RaJp	2524	10	2524	4	yes	2524	18
3: SoSuJp	2544	2662	2544	3600	no	2544	2829
3: SoRaJp	2544	3124	2544	3600	no	2544	3602 ∗
3: SuRaJp	2544	2562	2544	3600	no	2544	3312
3: SoSuRaJp	3882	1906	3882	2885	yes	3882	31

TABLE X: Head-to-Head With DeSyDe (Periods, Times in s)

Application	Hardware cost	$\mu$	Published bound	$t$ (s)
Sobel	16	384	400	0.5
SUSAN	12	1659	2050	0.5
RASTA	18	543	550	0.6

TABLE XI: Single-Application Benchmarks, Minimum Hardware Cost

Fig. 6: Decoupled flows against joint exploration per period bound: (a) instances proven to have no feasible design, (b) largest cost loss among the feasible ones (NP, equal to joint, not drawn). No pattern-first rule is both always feasible and never more expensive.

Fig. 7: Instances on which a decoupled flow is feasible but dearer than joint exploration, per period bound (the third count of Table XIII ). SL loses cost mostly at tight bounds, the timing-agnostic PF + mostly at loose ones.

Instance	Joint	SL	PF -	PF +	PF t	PF c	NP	Cores
p_rasta	3330	=	=	=	=	=	=	2
f_random_hw	3349	=	=	+25	=	=	=	5
d_random_hw	1857	=	=	+25	=	=	=	3
d_systematic_sw	1846	=	=	+163	=	=	=	2
f_sw3	3365	=	=	+41	+1038	=	=	4
f_both3	3406	=	=	=	+1038	=	=	5

TABLE XII: RQ2 Without a Period Bound (Extra Cost Over Joint)

Inputs	Bound	$n$	SL	PF -	PF +	PF t	PF c	NP
base	none	9	0/0/0.0	0/0/0.0	0/5/8.8	0/2/30.8	0/0/0.0	0/0/0.0
	$1.00\,\mu^{*}$	9	2/3/2.7	6/0/0.0	6/1/9.9	0/0/0.0	2/0/0.0	0/0/0.0
	$1.10\,\mu^{*}$	9	0/3/0.6	6/0/0.0	6/1/9.7	0/0/0.0	2/0/0.0	0/0/0.0
	$1.25\,\mu^{*}$	9	0/4/0.9	6/0/0.0	6/1/18.1	0/0/0.0	2/0/0.0	0/0/0.0
	$1.50\,\mu^{*}$	9	0/1/0.3	3/1/0.1	3/2/10.6	0/2/12.4	2/0/0.0	0/0/0.0
	$2.00\,\mu^{*}$	9	0/3/4.6	0/3/0.9	0/6/9.0	0/2/30.2	0/0/0.0	0/0/0.0

TABLE XIII: RQ2 per Input Variant and Period Bound: Infeasible / Dearer / Largest Loss (%)

SIL	FM	PF -	PF +	PF t	PF c
2	H	Low-SIL D/C	Low-SIL diverse D/C	Low-SIL D/C ‡	Low-SIL D/C ‡
2	S	Same-CPU D/C	Low-SIL diverse D/C	Same-CPU D/C	Same-CPU D/C
2	H+S	Low-SIL diverse D/C	Low-SIL diverse D/C	Low-SIL diverse D/C	Low-SIL diverse D/C
3	H	2-of-2 ‡	2-of-2	High-SIL isolated D/C	High-SIL isolated D/C
3	S	2-of-2	2-of-2	Mixed-SIL D/C	2-of-2
3	H+S	2-of-2 (2); 3-version (NVP) (2)	2-of-2 (2); 3-version (NVP) (2)	Mixed-SIL D/C (2); 3-version (NVP) (2)	2-of-2 (2); 3-version (NVP) (2)

TABLE XIV: Pattern Fixed by Each Pattern-First Rule (Base Inputs)

Fig. 8: Least period of each decoupled flow relative to the joint minimum period

\mu^{*}

(base inputs). The pattern-first rules that fix 2-of-2 for a SIL-3 actor need 1.45 to 1.55 times

\mu^{*}

; SL loses period only on the two instances without a SIL-3 actor.

Inputs	$\mu^{*}$	SL	PF -	PF +	PF t	PF c	NP
base	235–333	2, 1.09	6, 1.55	6, 1.55	0, 1.00	2, 1.55	0, 1.00
tok2	235–256	0, 1.00	0, 1.00	0, 1.00	0, 1.00	0, 1.00	0, 1.00
chk10	235–282	0, 1.00	6, 1.82	6, 1.82	0, 1.00	2, 1.55	0, 1.00
chk50	235–384	2, 1.13	6, 1.43	7, 1.43	2, 1.43	2, 1.43	0, 1.00

TABLE XV: Least Period per Flow: Instances Above

\mu^{*}

, Largest Ratio

Bound	Joint	SL	PF -	PF +	PF t	PF c	NP
none	5665	+0.4 %	+0.0 %	+0.4 %	+0.0 %	+0.0 %	+0.0 %
$1.00\,\mu^{*}_{z}$	$\infty$	$\infty$	$\infty$	$\infty$	$\infty$	$\infty$	$\infty$
$1.10\,\mu^{*}_{z}$	$\infty$	$\infty$	$\infty$	$\infty$	$\infty$	$\infty$	$\infty$
$1.25\,\mu^{*}_{z}$	5866	$\infty$	$\infty$	$\infty$	+0.0 %	+0.0 %	+0.0 %
$1.50\,\mu^{*}_{z}$	5852	$\infty$	+0.0 %	+0.0 %	+0.0 %	+0.0 %	+0.0 %
$2.00\,\mu^{*}_{z}$	5768	$\infty$	+0.0 %	+0.0 %	+0.0 %	+0.0 %	+0.0 %

TABLE XVI: Three Applications ( m_3app ) per Bound and Flow

Instance	Cores	$k$	Joint	Promotion	NP
p_rasta	2	1	$\infty$	–	$\infty$
f_random_hw	5	4	3634	293	$\infty$
		3	3919	586	$\infty$
		2	5506	2206	$\infty$
		1	$\infty$	–	$\infty$
d_random_hw	3	2	2297	448	$\infty$

TABLE XVII: Pattern Instances With a Bounded Core Count

Extension	Rows	Cheaper	Dearer	Pat.	Time
E1: doer one SIL lower	54	48 (1.9–19.6)	0	15	1.29
E2: priced diversity	54	6 (6.6–7.0)	9 (4.8–37.0)	10	1.03
E1 and E2	54	38 (3.1–18.5)	4 (5.8–9.8)	11	1.26
E3, $\kappa=1$	45	0	0	3	1.02
E3, $\kappa=1.5$	45	2 (8.9–11.5)	0	5	1.13
E3, $\kappa=2$	45	28 (0.1–22.2)	0	15	1.33

TABLE XVIII: Model Extensions Against the Model (Joint Optima)

Model	SL	PF -	PF +	PF t	PF c
E1+E2, inf.	2/0/0/0/0	6/6/6/3/0	6/6/6/3/0	0/0/0/0/0	0/0/0/0/0
loss (%)	5.9	23.2	46.3	0.0	0.0
E3, $\kappa=1$ , inf.	2/0/0/0/0	6/6/6/3/0	6/6/6/3/0	0/0/0/0/0	2/2/2/2/0
loss (%)	4.6	0.9	18.1	30.2	0.0
E3, $\kappa=1.5$ , inf.	2/0/0/0/0	6/5/5/0/0	6/5/5/0/0	0/0/0/0/0	2/2/2/0/0
loss (%)	13.1	0.9	18.1	30.2	0.0

TABLE XIX: Decoupled Flows Under the Extended Models

Fig. 9: Solve time on synthetic instances, one mark per graph (counts in Table XX ). Filled: proven optimal; open: time limit reached; cross: no period bound

\mu^{*}

found, so no cost solve. Beyond 16 actors, most searches reach a limit.

Fig. 10: Cost of flattening the throughput model of the synthetic graphs (median per actor count, logarithmic axes): compile time and FlatZinc size both grow steeply with the number of HSDF actors.

Actors	Graphs	$\mu^{*}$ found	$\mu^{*}$ proven	Proven	Time limit	No $\mu^{*}$	Median (s)	Flatten (s)	FlatZinc (MB)	Memory (MB)
8	5	5	5	5	0	0	1.8	0.8	2	44
16	5	5	4	5	0	0	56.1	2.9	8	86
24	5	5	2	2	3	0	84.9	8.3	20	173
32	4	4	0	1	3	1	273.7	15.8	36	305
48	–	0	0	–	–	5	–	61.9	116	736
64	–	0	0	–	–	5	–	139.0	252	1588

TABLE XX: RQ3 Actor Sweep: Outcome, Solve Time, and Model Size

Fig. 11: Extra cost of the cheapest one-core design of the running example without patterns over its optimum, per cost profile and hardware price factor. Only the flat profiles reach zero (one core optimal).

Fig. 12: Total cost of the optimum with at most

k

cores, running example without patterns at four times the hardware prices. The steep profiles pay heavily for the third consolidation step; Klosterman’s profile hardly at all.

Profile	$\times$	Opt. (cores)	$k\leq 3$	$k\leq 2$	$k\leq 1$	Pro.
Myklebust et al.	1	1914 (3)	1914	2199	3786	1913
	2	2115 (3)	2115	2392	3946	1913
	4	2517 (3)	2517	2778	4266	1913
	8	3321 (3)	3321	3550	4906	1913
	16	4929 (3)	4929	5094	6186	1913
Klosterman	1	1116 (3)	1116	1148	1350	275

TABLE XXI: Hardware Price Sweep per Cost Profile (Total Cost)

	c_pat			pc_sobel
Variant	$\|G^{+}\|$	$C_{\mathrm{tot}}$	$\mu^{*}$	$\|G^{+}\|$	$C_{\mathrm{tot}}$	$\mu^{*}$
TDMA bus (default)	71	3349	235	57	1401	333
ideal bus	26	3349	235	15	1401	333
--comm-sil inherit	71	5246	277	57	2608	333
--comm-sil core	71	3349	235	57	1401	333
--comm-scope all	392	3349	279	270	1401	369

TABLE XXII: Communication Variants

	H	H+S	NVP (H+S)
elements	117	151	165
goals	41	54	54
undeveloped goals	15	20	20
Solutions	16	19	33
leaves	31	39	53
Solutions among leaves (%)	52	49	62

TABLE XXIII: Statistics of the Generated Arguments

Instance	CP-SAT (4)	Gecode	HiGHS	Chuffed
p_rasta	3330	–	–	err.
f_random_hw	3349	–	–	err.
d_random_hw	1857	–	2585	err.
d_systematic_sw	1846	–	✓	err.
f_sw3	3365	–	5470	err.
f_both3	3406	–	4349	err.

TABLE XXIV: Cross-Solver Runs on the Instances of Table VIII

Mutation (what it breaks)	Mutants	First	Current
a placement relation of the selected pattern	32	32	32
a node’s SIL below its requirement	50	50	50
a core’s provisioned SIL below a node’s	39	39	39
a core SIL above its type’s ceiling	21	21	21
two SILs on an unpartitioned core	23	23	23
a reported period below the MCR	12	12	12

TABLE XXV: Corrupted Solutions per Operator: Rejected by the Verifier

Constraint family removed	Runs	Viol.	First	Current
placement relations, 10	10	9	9	9
node SIL $\geq$ requirement, 7	10	10	10	10
node SIL $\leq$ core SIL, 7	10	0	0	0
core SIL $\leq$ type ceiling, 7	10	7	7	7
SIL-mixing rule, 8	10	10	10	10
partitioning capability, 7	10	9	0	9

TABLE XXVI: Model Mutants per Constraint Family

Part	Defect	Found by	Resolution
Model	Implied constraint on heavy node pairs ignored activity, so an owner could not share a core with its own inactive slot; the front-end’s least core count also counted slots	tight bounds made instances with a verified design infeasible	guarded by the activity of both nodes; core count from always-active nodes
Model	Recurring pattern cost counted once per slot of an actor	reading the model for the paper	summed over application actors only
Model	No-promotion rule also bound inactive slots, which then had to be active	every NP solution activated all slots	rule guarded by activity; NP re-run, now equal to joint
Model	A path through an inactive slot can raise a design’s least period above its MCR	verifier rejected two time-limited incumbents by period	documented; exact variants kept as patches and used as a cross-check ( Section IV-E )
Front-end	Slots shared by position between patterns, so a checker took a replica’s WCET and the reverse	a slot whose role and WCET type differed	slots shared only by equal WCET type; all RQs re-run
Front-end	Owner type of a replica not found for a multi-rate owner	building multi-rate synthetic graphs	lookup in the owner’s application, ignoring the copy suffix; regression test

TABLE XXVII: Defects Found While Running the Evaluation, and Their Fixes

Appendix figures & tables2 assets

Supplementary material from the paper’s appendix.

Appendix

Instance	Application(s)	Platform file	Fault model	Bus	Remarks
p_rasta	RASTA	mixed.xml	H	ideal	certified partitioning on the R-card
f_random_hw	RASTA	mixed_noiso.xml	H	ideal	–
d_random_hw	RASTA	mixed_noiso.xml	H	ideal	SIL 3 actors lowered to SIL 2
d_systematic_sw	RASTA	mixed_noiso.xml	S	ideal	SIL 3 actors lowered to SIL 2
f_sw3	RASTA	mixed_3type.xml	S	ideal	–
f_both3	RASTA	mixed_3type.xml	H+S	ideal	–

Appendix

TABLE XXVIII: Inputs of the Pattern Instances

Experiment	Driver	CSV ( experiments/results/ )	Used in
RQ1 benchmarks	harness.py rq1	e1_parity	Table XI
RQ1 DeSyDe	desyde_cmp.py , desyde/build.sh	e7_desyde , e7_safedse	Table X
RQ2 flows	harness.py rq2 , rq2tight , rq2thr , rq2var , rq2reps , pftable	e2_joint , e2_tight , e2_thr , e2_var , e2_reps , e2_pfchoice	Figs. 6 , 7 and 8 , Tables XII , XIII , XV and XIV
RQ2 certificates	certify_pf.py	e2_cert	Section VI-C
RQ2 exactness	exact_model.py , exact_check.py	e2_exact , e2_exact_sl	Section VI-C
Three applications, promotion	breadth.py multi , patcons	e5_multi , e5_multi_exact , e5_multi_exact_long , e4_patcons	Tables XVI and XVII

Appendix

TABLE XXIX: Experiments, Drivers, Data, and Where They Appear

Real-Time Scheduling

Real-time scheduling allocates processors, accelerators, and network resources so tasks meet timing deadlines under workload and resource constraints.

See all 30 papers

Jun 4, 2026

Data Flow Control: Data Safety Policies for AI Agents

Agents increasingly generate SQL, orchestrate pipelines, and automate data analysis on behalf of users. While recent work improves query correctness, correctness is not safety. A query may be semantically valid yet violate regulatory, privacy, or business constraints that govern how data may be combined and released. We argue that enforcing such constraints is fundamentally a data infrastructure problem. This paper introduces Data Flow Control (DFC), a framework to declaratively specify and guarantee policy enforcement over tuple-level data flows within a DBMS query. A key challenge is defining a policy language that is optimizer-invariant yet efficient to enforce at scale. We formalize data safety as aggregate predicates over provenance monomials and present Passant, a portable query rewriting layer that enforces DFC policies without materializing provenance. Across five DBMS engines -- DuckDB, Umbra, PostgreSQL, DataFusion, and SQLServer -- Passant achieves ~0% overhead and outperforms alternatives by orders of magnitude. As a result, Data Flow Control is the first step towards moving data safety from prompts and post-hoc checks into the data infrastructure. Data Flow Control is available open source at https://github.com/dataflowcontrol/data-flow-control.

Charlie Summers, Eugene Wu

Columbia University New York, New York, USA

AI Agent Security Information Flow Control Access Control

Ask PDF

Sep 10, 2026

DeFiFlowBench: Benchmarking and Improving Safe Executability in Natural-Language DeFi Workflow Synthesis

A structurally valid DeFi workflow can still authorize a costly trade. We introduce DeFiFlowBench, a benchmark of 207 team-authored prompts for natural-language DeFi workflow synthesis. It measures graph coverage, configuration completeness, and declared safety predicates, then tests supported trade configurations on a local EVM. Direct, constrained, and few-shot prompting produce 14-19 unsafe held-out executions per configuration under a fixed 5% price-impact cap. A slippage bound derived from a quote does not prevent the price impact of the order itself. We propose Koan-Safe, which combines a prompt-only intent parser, a replaceable generator, and structural repair with default safety parameters. On 75 held-out workflow prompts, its hybrid variant scores 0.67 on the static safety proxy, compared with 0.33 for the best baseline. Koan-Safe records no unsafe executions on the saved benchmark outputs. A matched-candidate ablation produces 14-17 unsafe executions when enforcement is disabled. Additional tests expose the limits of default injection: permissive existing thresholds can still authorize unsafe trades. A separately evaluated policy cap addresses this failure on a 36-case diagnostic grid. These results support explicit trade protections and execution-based evaluation, while distinguishing declared safety from a general guarantee.

Abhinav Rajeev Kumar, Harshit Arora, Varun Singh +1

SRM Institute of Science and Technology

LLM Safety Benchmarks LLM Guardrails Decentralized Finance LLM Safety Evaluation

Ask PDF

Jul 24, 2026

What Can Be Enforced? A Theory of Certified Runtime Safety for Tool-Using Agents

Runtime guardrails act before irreversible tool calls, but their guarantees depend on what policy state is representable, what a judge observes, and whether intervention changes future behavior. We separate three questions. First, relative to fixed oracle predicates, a deterministic gate enforces exactly the nonempty safety policies whose good prefixes its register model recognizes; policy nontriviality is undecidable with two decrementable counters but in PSPACE for a separable monotone fragment. Second, under a fixed exogenous law, Neyman-Pearson gives the exact false-block/miss frontier and conformal calibration gives a finite-sample marginal certificate, possibly via block-all. Third, once blocking changes future proposals, static scores and ungated trajectories need not identify the closed-loop frontier; a specified finite controlled model instead yields an occupancy program. Bounded representation attacks add a robustness margin, so benign calibration alone does not transfer. Experiments target these distinctions through static diagnostics, controlled-model enumeration, representation rewrites, and paired closed-loop reruns.

Shawn Ray

Carnegie Mellon University

Runtime Enforcement for AI Agents Runtime Assurance LLM Agent Safety

Ask PDF

Abstract

Real-Time Scheduling

Explore similar work

Data Flow Control: Data Safety Policies for AI Agents

DeFiFlowBench: Benchmarking and Improving Safe Executability in Natural-Language DeFi Workflow Synthesis

What Can Be Enforced? A Theory of Certified Runtime Safety for Tool-Using Agents