{"id":"03bc445d-067f-44f9-874d-0e5db8e4b266","arxiv_id":"2506.14581","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper contributes transformation rules that map new stochastic Simulink subsystems (timer, switch, sampling, noise, aging) into stochastic hybrid automata, enabling statistical model checking of uncertain embedded control systems.","lead":"This paper adds a library of Simulink blocks that model uncertainty, such as sensor noise, aging, and random failures, and translates those blocks into stochastic hybrid automata for formal analysis. The authors show the translation on two small case studies, comparing fast statistical model checking on the automata with slower Simulink simulation.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The templates' semantics preservation is unproven, and the evaluation validates only hand-optimized automata, so the central transformation claim lacks direct support.","rationale":"The reader's CONDITIONAL verdict is appropriate. The paper contributes a useful library and lifted composition, and the two case studies show plausible evidence. However, the central claim requires that the SHA templates preserve the stochastic behavior of the Simulink subsystems; this is asserted but not proven. The hand-optimized evaluation makes the gap concrete: whatever the CIs in Tables 1 and 2 show, they cannot validate the transformation rules unless the automatically generated automata are shown to be equivalent to the hand-optimized ones. The switch template's clock initialization is a good focus because it is a place where the HAwK encoding and the informal Simulink description differ in mechanism; even if the laws coincide for the constant distributions used, the paper needs an explicit argument. This is an addressable gap rather than a fatal flaw, so the verdict should remain CONDITIONAL.","tokens_in":20342,"tokens_out":12021,"duration_ms":132469,"concrete_test":"Formalize the subsystem semantics of Sec. 3 (timer falling-edge re-trigger; switch alternating timers) as a stochastic process and prove a stochastic simulation relation with the HAwK templates in Fig. 6a and Fig. 6b for the supported U(low,high) and folded-normal distributions. In particular, the proof must account for the switch template's sampling of the inactive timer's expiration at time 0 rather than at the switching instant; if the proof cannot be completed, or a counterexample is found for the supported distributions, the transformation is not semantics-preserving and the Sec. 7 claim is unsupported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim (Sec. 7) is that the SHA templates of Sec. 4.2, composed via the lifted rules of Sec. 4.1, let us formally analyze safety and performance under uncertainty. The load-bearing premise is that each template is semantics-preserving with respect to the Simulink subsystem it represents. The paper gives no equivalence proof, and the evaluation does not exercise the transformation: the HAwKs in Figs. 10 and 12 are hand-optimized versions of the automatically derived automata, as stated in Sec. 5, so the agreement between modes and Simulink CIs in Tables 1 and 2 supports only those hand-built automata, not the transformation rules. A concrete semantic subtlety is visible in the stochastic switch template (Fig. 6b): the expiration time for the timer that is currently inactive is sampled at the initial state (or at the previous switch), not at the moment the active timer expires; because the inactive random clock has rate 0 this yields the correct dwell-time distribution for the constant, state-independent distributions used here, but this equivalence is neither stated nor proved, and it would fail for state-dependent delay kernels. The missing proof is exactly what is needed to transfer the quantitative results back to the original Simulink models.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents an approach for modeling uncertainties in Simulink by providing a library of stochastic subsystems (Stochastic Timer, Switching, Sampling, Noise, Discrete Aging, Continuous Aging) and formalizing them as stochastic hybrid automata (SHA). The authors extend a previously proposed Simulink-to-SHA transformation by lifting the parallel composition rules from LHACsync to HAwKsync and by giving SHA templates, called HAwK templates, for each stochastic subsystem. The approach is intended to enable quantitative analysis, such as statistical model checking, of Simulink models under uncertainty. The evaluation applies the resulting automata to two case studies, a temperature control system with sensor loss and an energy measurement unit with stochastic switching, comparing confidence intervals obtained from the modes statistical model checker with confidence intervals computed from Simulink simulation.","tokens_in":20625,"tokens_out":12301,"duration_ms":123534,"significance":"If the transformation rules are correct, the paper addresses a real and practically important gap: bringing stochastic uncertainties in Simulink models into a formal framework that supports quantitative verification. The proposed subsystem library is well motivated, the paper includes concrete HAwK templates for each subsystem, and the two case studies demonstrate a significant runtime advantage for the SHA-based analysis. The authors provide an artifact with models and scripts, which is a definite strength. The main limitation is that the central formalization claim is currently not substantiated: no correctness statement or proof links the semantics of the stochastic Simulink subsystems to the HAwK templates, and the empirical evaluation uses hand-optimized automata rather than the automatic transformation output. One quantitative result in Table 1 is also inconsistent with the accompanying text. These issues affect the load-bearing claim that quantitative results on the SHA transfer back to the original Simulink models.","major_comments":[{"comment":"The paper states that the SHA templates 'formalize' the stochastic Simulink subsystems, but it gives no equivalence statement or proof. For instance, the stochastic timer template in Fig. 6a replaces the Simulink falling-edge re-trigger with an immediate self-loop resampling, and the stochastic switch template in Fig. 6b collapses two interacting timers into edge delays. It is not shown that the stochastic process induced by the HAwK is equivalent to the stochastic process induced by the corresponding masked Simulink subsystem, in either a distributional or a trace-based sense. This is load-bearing for the abstract's claim that the approach 'allows us to formally argue about safety and performance under uncertainty', because results obtained on the SHA can be transferred to the Simulink model only if the transformation is semantics-preserving. Please provide a precise correctness theorem (e.g., equivalence of reachability probabilities or of the induced stochastic processes) and its proof, or a clearly stated set of assumptions under which the templates are exact, together with a proof under those assumptions.","section":"Sec. 4.2, Figs. 6-8"},{"comment":"The evaluation does not exercise the proposed transformation. The text says that the HAwKs shown in Figs. 10 and 12 have been hand-optimized to eliminate redundant or unused variables, locations and edges, so the confidence intervals in Tables 1 and 2 validate only those hand-built automata, not the automatic transformation rules of Sec. 4. Furthermore, Table 1 contradicts the accompanying sentence that all modes CIs lie within the Simulink CIs: for P(◇ tmp ≤ 20), modes reports [0.0497, 0.05885] while Simulink reports [0.0652, 0.0795], and the two intervals are disjoint. This is precisely the kind of discrepancy that would signal a semantic mismatch between the SHA and the Simulink model, and the paper does not discuss it. Please either run the unoptimized automatic transformation in the evaluation, or give a semantics-preservation argument for the applied optimizations, and in either case address the non-overlapping interval in Table 1.","section":"Sec. 5, Tables 1-2"},{"comment":"In the stochastic switch template, the expiration time of the clock that is currently inactive is sampled at the initial state or at the previous switch and then frozen, because the inactive random clock has rate 0. In the Simulink subsystem of Fig. 3b, the expiration time of the other timer is sampled anew at the instant the active timer expires. For the constant, state-independent distributions U(low,high) and N≥0 considered in the paper, the two mechanisms yield the same dwell-time distribution, but this equivalence is neither stated nor proved, and it fails if the delay kernels are made state-dependent, which the HAwK definition (Def. 2) allows. Please state explicitly that the templates are intended only for state-independent delay distributions and give the distributional equivalence argument, or modify the template so that resampling occurs at the correct state.","section":"Sec. 4.2, Fig. 6b"},{"comment":"The lifted composition rules for HAwKsync do not specify how the label of the resulting synchronized edge is chosen, nor how the random clock of a receiving edge is eliminated. In a HAwK, delay kernels are indexed by labels and each label has exactly one random clock; after synchronizing edges with different delay kernels, the receiving edge's clock must be handled consistently, and labels must be renamed so that the guard-disjointness condition for equal labels is preserved. Without this detail, the composed object is not unambiguously a HAwK, and the claim in Sec. 4.1 of a seamless integration into the existing transformation is not fully substantiated. The rules should be completed and, preferably, accompanied by a correctness argument for the composition itself.","section":"Appendix A.3, Definitions 5-6"}],"minor_comments":[{"comment":"The sentence 'Init assigns a pair of initial state and condition to each location l in Loc for each v in Varoutput' appears to mean that Init assigns the pair to each location, not to each variable; please rephrase.","section":"Appendix A.3, Definition 4"},{"comment":"Item 5 uses the undefined symbols Lsync,i and Lcomp; these should likely be Synci and Acomp, respectively.","section":"Appendix A.3, Definition 6"},{"comment":"For synchronized edges, the text says the delay kernel from the sending edge is assigned to the new edge, but it does not state what happens to the delay kernels of the receiving edges; please clarify whether they are discarded and why this is correct.","section":"Sec. 4.1"},{"comment":"The text describing the stochastic noise template refers to edges e0-e3 while the figure appears to use e1-e3 inconsistently; please align the figure and the text.","section":"Fig. 7b and Sec. 4.2"},{"comment":"Please report the number of modes runs for the energy measurement case study as well, and state the seeds and schedulers used for both case studies, so that the experiments are fully reproducible.","section":"Sec. 5, Tables 1-2"}],"recommendation":"major_revision","confidential_remarks":"The non-overlapping confidence interval in Table 1 for P(◇ tmp ≤ 20) deserves close scrutiny; if it persists after additional runs or with the unoptimized transformation, it may indicate a genuine semantic mismatch in the stochastic sampling template or in the hand-optimization step, rather than mere sampling noise. The missing correctness proof is the main technical gap and should be a condition for acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper is worth reading if you work on formalizing Simulink semantics or on SMC for industrial models. It adds a small library of six stochastic Simulink subsystems (timer, switching, sampling, noise, discrete aging, continuous aging) and, more importantly, gives HAwK templates for each, plus composition rules that lift the authors' earlier LHACsync composition to HAwKsync. That is a genuine extension: the earlier transformation only handled simplified failure-repair models, and the existing SMC-on-Simulink approaches do not produce a formal automaton. The two case studies are small, but the speedups are real—0.3 s for modes versus 30 minutes and 12 minutes for Simulink—and the CIs mostly overlap fine. The artifact is available and the presentation is clear.\n\nThe soft spots are the ones you'd expect. There is no proof that the templates preserve the Simulink subsystem semantics. The paper states the transformation rules as formal templates, but equivalence is asserted, not demonstrated. That matters because the SHA templates are what give access to “formally argue about safety and performance.” The authors are honest about the evaluation: the HAwKs in Figs. 10 and 12 are hand-optimized versions, not the direct output of the automated transformation. So the empirical agreement validates those hand-built automata, not the transformation rules themselves. The one partial overlap (P(◇ total ≥ 16000)) is also acknowledged and plausibly a sampling artifact, but it is a reminder that the evidence is not overwhelming.\n\nThere is a specific semantic subtlety in the stochastic switch template that supports these concerns: the expiration time for the inactive timer is sampled at the initial state (or previous switch), not when the active timer expires. For the constant, state-independent distributions used in the case studies this is fine, but it is not stated or proved, and it would break for state-dependent delay kernels. That is the kind of detail that a proof or a counterexample would settle.\n\nOverall, this is a credible, useful extension, not a breakthrough. The central idea holds up in the demonstrated setting, but the missing semantics-preservation proof is the load-bearing gap between “we transformed the model” and “we formally analyzed the Simulink model.” I would send it to serious referees with a request that the authors either provide an equivalence argument or adjust the claims to what is actually shown. A revised version that runs the transformation end-to-end on the case studies would answer most of the worry.","headline":"A useful, well-scoped extension of Simulink-to-SHA transformation, but the missing semantics-preservation proof leaves the central formal claim only conditionally supported.","tokens_in":21113,"tokens_out":2635,"would_cite":true,"duration_ms":25658,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that stochastic Simulink subsystems can be transformed into stochastic hybrid automata, enabling formal quantitative analysis of safety and performance under uncertainty.","keywords":["Simulink","Stochastic Hybrid Automata","Uncertainty","Statistical Model Checking","Safety analysis","Performance analysis","Model transformation","HAwK"],"falsifier":"Feed the same distribution parameters to the stochastic timer block in Simulink and to the corresponding HAwK template, run both with the same input for many repetitions, and compare the empirical distribution of expiration times: the Simulink falling-edge re-trigger and the template's immediate self-loop resampling should produce identical timer-value traces if the semantics match. A more direct test is to run the automatic transformation end-to-end without the hand-optimizations described in the evaluation and check whether the confidence intervals for the energy-unit property $P(\\lozenge\\, total \\geq 16000)$ still overlap those from Simulink, since that is the property where the current results only partially overlap.","tokens_in":20118,"feed_emoji":"⚙️","tokens_out":6964,"duration_ms":63658,"temperature":0.7,"pith_summary":"Simulink is widely used for embedded control design, but its semantics are informal and its models usually ignore uncertainty such as sensor noise, aging, and failures. This paper tries to close that gap by providing six parameterizable Simulink subsystems that inject stochastic behavior, and by giving transformation rules that turn each subsystem into a stochastic hybrid automaton (SHA) template. The templates compose with an existing Simulink-to-SHA transformation, so the resulting formal model can be analyzed with statistical model checking and reachability analysis rather than by expensive simulation alone. On two small case studies, the SHA-based analysis produces confidence intervals that agree with Simulink simulation while running orders of magnitude faster. If the transformation is faithful, engineers could get formal, probabilistic safety and performance guarantees for Simulink models that include realistic uncertainties.","feed_headline":"Uncertain Simulink models gain formal probabilistic analysis","feed_subtitle":"New transformation rules turn stochastic Simulink subsystems into automata that statistical model checking can verify.","key_machinery":"The central object is the HAwK, a hybrid automaton with stochastic kernels: delay kernels sample the expiration time of each random clock, and reset kernels stochastically reassign continuous variables at discrete steps. On top of this, the paper defines HAwKsync templates, which add sending and receiving labels and separate input from output variables, so each Simulink subsystem becomes a small automaton. The load-bearing templates are the stochastic timer (a location where the output decreases at rate $-1$ and a self-loop resamples the output from the configured distribution) and the stochastic switch (two random clocks, one per input, whose expiration decides which input is passed to the output). The lifted parallel-composition rules combine templates: for synchronized edges the delay kernel comes from the sending edge and the reset kernels from all involved edges are merged, which is well-defined because each template owns its output variables. This machinery is what lets a composed SHA inherit both the continuous dynamics and the probabilistic behavior of the original Simulink model.","core_discovery":"The paper's central claim is that the stochastic Simulink subsystems it defines have exact formal counterparts as HAwK templates, and that composing these templates with the lifted parallel-composition rules yields a monolithic stochastic hybrid automaton whose quantitative behavior matches the Simulink model. The paper presents templates for a stochastic timer, a stochastic switch, stochastic sampling, stochastic noise, and discrete and continuous aging, including variants with and without explicit repair signals. The delay and reset kernels of HAwK encode the random expiration times and the stochastic reassignments of variables, respectively. The evaluation compares statistical model checking on the automaton with simulation of the original Simulink models for a temperature control system with sensor loss and an energy measurement unit with stochastic switching. For most properties the confidence intervals from the automaton lie within those from Simulink simulation, with much smaller computational cost, and the paper concludes that this enables formal reasoning about safety and performance under uncertainty.","pith_inferences":["If the template semantics are later proved or validated, the same template pattern could be extended to other stochastic Simulink constructs such as Poisson arrivals, discrete random walks, or correlated noise, turning the library into a general uncertainty modeling language.","The evaluation's hand-optimized automata suggest that the automatic composition may currently produce larger or less efficient models; an automated end-to-end pipeline with equivalence checking would be needed before industrial deployment.","The rare-event property where the confidence intervals only partially overlap indicates that very small probabilities may be sensitive to the sampling tick or scheduler choice; rare-event simulation techniques could be combined with the SHA to sharpen those estimates.","A direct comparison between statistical model checking and a reachability analysis on the same SHA would test whether the stochastic guarantees extend beyond the SMC setting the paper evaluates."],"forward_implications":["If the templates are faithful, safety properties such as 'the temperature never drops below 20' can be checked on the SHA with statistical model checking, and the resulting probability estimates transfer to the Simulink model.","Engineers can use the parameterizable subsystem library to inject aging, noise, sensor loss, or stochastic switching into existing Simulink models and still obtain formal, quantitative guarantees, instead of relying on the idealized model.","Because the SHA analysis ran in about 0.3 seconds versus 30 minutes for the temperature case and 12 minutes for the energy case, the approach makes it practical to run far more samples and obtain tighter confidence intervals.","The same composed SHA is not limited to statistical model checking; it is also a candidate for reachability analysis, so the paper's transformation opens the door to analysis techniques beyond simulation."],"supporting_citations":[{"why":"Supplies the base modular transformation from Simulink to LHAC/SHA that the stochastic subsystem templates extend.","marker":"[8]"},{"why":"Defines the decomposed hybrid automaton semantics with delay and reset kernels that HAwK builds on.","marker":"[35]"},{"why":"Introduces the decomposed HA formalism and stochastic specification approach the paper adapts into HAwK.","marker":"[34]"},{"why":"Provides the statistical model checker used to compute confidence intervals for the SHA case studies.","marker":"[9]"},{"why":"Provides the Wilson-score based method used to compute comparable confidence intervals from Simulink simulation.","marker":"[1]"},{"why":"Identifies the catalogue of uncertainty sources (noise, aging, failures, clock errors) that motivates the subsystem library.","marker":"[7]"}],"fun_headline_variants":["Simulink uncertainty captured by stochastic hybrid automata","Formal verification path from Simulink to stochastic automata","Transforming uncertain Simulink into analyzable SHA","Statistical model checking for uncertain Simulink models","Closing gap between Simulink and formal analysis under uncertainty"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that each SHA template faithfully formalizes the semantics of its Simulink subsystem, especially the stochastic timer's immediate self-loop resampling and the stochastic switch's two-timer edge delays, and the paper gives no equivalence proof to back that premise.","fun_headline_variants_meta":{"raw":{"variants":["Simulink uncertainty captured by stochastic hybrid automata","Formal verification path from Simulink to stochastic automata","Transforming uncertain Simulink into analyzable SHA","Statistical model checking for uncertain Simulink models","Closing gap between Simulink and formal analysis under uncertainty"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00075,"raw_usage":{"total_tokens":3314,"prompt_tokens":897,"completion_tokens":2417,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":513,"completion_tokens_details":{"reasoning_tokens":2338}},"tokens_in":513,"tokens_out":2417,"duration_ms":16644,"temperature":1.0,"reasoning_tokens":2338,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T19:51:14.648438+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Feed the same distribution parameters to the stochastic timer block in Simulink and to the corresponding HAwK template, run both with the same input for many repetitions, and compare the empirical distribution of expiration times: the Simulink falling-edge re-trigger and the template's immediate self-loop resampling should produce identical timer-value traces if the semantics match. A more direct test is to run the automatic transformation end-to-end without the hand-optimizations described in the evaluation and check whether the confidence intervals for the energy-unit property $P(\\lozenge\\, total \\geq 16000)$ still overlap those from Simulink, since that is the property where the current results only partially overlap.","supporting_citations":[{"cited_title":"In: Integrated Formal Methods","cited_arxiv_id":null,"evidence_quote":"Supplies the base modular transformation from Simulink to LHAC/SHA that the stochastic subsystem templates extend."},{"cited_title":"In: Principles of Verification: Cycling the Probabilistic Landscape : Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday, Part III","cited_arxiv_id":null,"evidence_quote":"Defines the decomposed hybrid automaton semantics with delay and reset kernels that HAwK builds on."},{"cited_title":"In: Quantitative Evaluation of Systems - 20th Modeling Uncertainty in Simulink and SHA 25 Int","cited_arxiv_id":null,"evidence_quote":"Introduces the decomposed HA formalism and stochastic specification approach the paper adapts into HAwK."},{"cited_title":"In: 24th Int","cited_arxiv_id":null,"evidence_quote":"Provides the statistical model checker used to compute confidence intervals for the SHA case studies."},{"cited_title":"In: Bridging the Gap Between AI and Reality","cited_arxiv_id":null,"evidence_quote":"Provides the Wilson-score based method used to compute comparable confidence intervals from Simulink simulation."},{"cited_title":"In: Leveraging Applications of Formal Methods, Verification and Validation","cited_arxiv_id":null,"evidence_quote":"Identifies the catalogue of uncertainty sources (noise, aging, failures, clock errors) that motivates the subsystem library."}],"review_version":2}