Shaokai Lin

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2026-211

May 19, 2026

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2026/EECS-2026-211.pdf

Cyber-physical systems (CPS) are increasingly deployed in safety-critical domains such as autonomous vehicles, avionics, and industrial automation, yet today’s toolchains rarely connect correctness, timing analysis, and implementation in one coherent workflow. Classical timing analysis does not directly support the notion of logical time, the abstraction used by deterministic CPS coordination languages; most formal verification tools do not analyze CPS engineering models directly and remain labor-intensive to apply; and hard real-time guarantees often depend on schedules crafted by hand, which is slow and error-prone. Can we design a toolchain that closes all three gaps in a unified workflow?

This thesis develops an affirmative answer through a suite of design-time analysis, formal verification, and scheduling techniques for cyber-physical systems, built on the reactor model of computation and the Lingua Franca coordination language.

The contributions are:

• A system-level timing and trade-off analysis framework that extends the CAL theorem (consistency, availability, latency) to the reactor model and supports dynamic execution traces. A central proposition expresses each reaction’s physical firing time as a max-plus linear recurrence over a system matrix whose eigenvalue identifies the critical path of a distributed program, enabling principled derivation of decentralized coordination parameters in place of manual hand-tuning.

• A perspective on engineering and scientific modeling in formal verification. Formal verification reasons only about formal models, so one must distinguish which parts of a model specify intended behavior (engineering models) from which parts approximate implementations or environments (scientific models), and interpret verification results accordingly. The two roles should not be conflated without keeping that distinction clear. We demonstrate this perspective through an encoding of Lingua Franca’s deterministic semantics in Timed Rebeca, and argue that TR’s timing features are better suited to engineering modeling than to scientific modeling.

• The LF Verifier, the first fully automated verifier for Lingua Franca programs, which encodes reactor systems’ behavior as axiomatic models sound for all valid runtime implementations, computes bounded model checking completeness thresholds, and automatically translates C reaction bodies into Uclid5 axioms. On a benchmark suite of 22 programs, it correctly verifies 21 fully automatically.

• State Space Finite Automata (SSFA), a unified formalism for quasi-static scheduling of deterministic timed concurrent models, subsuming synchronous dataflow, scenario-aware dataflow, and logical execution time. Integrated into the Lingua Franca compiler and executed by the PretVM runtime, quasi-statically scheduled programs reduce average runtime overhead by 9× over dynamic scheduling while providing anomaly-free timing and analyzable worst-case makespan without requiring per-step worst-case execution times. An integration with Mocasin further enables compile-time design space exploration over time–energy trade-offs on heterogeneous platforms.

• A modernized implementation of GameTime, a timing analysis tool that combines game-theoretic online learning and systematic testing using satisfiability modulo theories (SMT) solvers. GameTime can estimate worst-case execution times of reaction bodies as well as answer other timing analysis questions. Rebuilt on LLVM and KLEE and supporting cycle-accurate emulation on FlexPRET, it supplies timing estimates for sequential programs consumed by the system-level and quasi-static analyses above, closing the loop between design-time reasoning and the actual execution-time behavior of generated code.

These contributions form a toolchain that connects analyzable CPS models, automated verification at the engineering level, and quasi-static scheduling into deterministic, verifiably correct, high-performing implementations.

Advisors: Edward A. Lee and Sanjit A. Seshia

---

BibTeX citation:

@phdthesis{Lin:EECS-2026-211,
    Author= {Lin, Shaokai},
    Title= {Verifiable Cyber-Physical Systems: Building Engineering Models for Deterministic and Predictable Concurrent Execution},
    School= {EECS Department, University of California, Berkeley},
    Year= {2026},
    Month= {May},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2026/EECS-2026-211.html},
    Number= {UCB/EECS-2026-211},
    Abstract= {Cyber-physical systems (CPS) are increasingly deployed in safety-critical domains such as autonomous vehicles, avionics, and industrial automation, yet today’s toolchains rarely connect correctness, timing analysis, and implementation in one coherent workflow. Classical timing analysis does not directly support the notion of logical time, the abstraction used by deterministic CPS coordination languages; most formal verification tools do not analyze CPS engineering models directly and remain labor-intensive to apply; and hard real-time guarantees often depend on schedules crafted by hand, which is slow and error-prone. Can we design a toolchain that closes all three gaps in a unified workflow?

This thesis develops an affirmative answer through a suite of design-time analysis, formal verification, and scheduling techniques for cyber-physical systems, built on the reactor model of computation and the Lingua Franca coordination language.

The contributions are:

• A system-level timing and trade-off analysis framework that extends the CAL theorem (consistency, availability, latency) to the reactor model and supports dynamic execution traces. A central proposition expresses each reaction’s physical firing time as a max-plus linear recurrence over a system matrix whose eigenvalue identifies the critical path of a distributed program, enabling principled derivation of decentralized coordination parameters in place of manual hand-tuning.

• A perspective on engineering and scientific modeling in formal verification. Formal verification reasons only about formal models, so one must distinguish which parts of a model specify intended behavior (engineering models) from which parts approximate implementations or environments (scientific models), and interpret verification results accordingly. The two roles should not be conflated without keeping that distinction clear. We demonstrate this perspective through an encoding of Lingua Franca’s deterministic semantics in Timed Rebeca, and argue that TR’s timing features are better suited to engineering modeling than to scientific modeling.

• The LF Verifier, the first fully automated verifier for Lingua Franca programs, which encodes reactor systems’ behavior as axiomatic models sound for all valid runtime implementations, computes bounded model checking completeness thresholds, and automatically translates C reaction bodies into Uclid5 axioms. On a benchmark suite of 22 programs, it correctly verifies 21 fully automatically.

• State Space Finite Automata (SSFA), a unified formalism for quasi-static scheduling of deterministic timed concurrent models, subsuming synchronous dataflow, scenario-aware dataflow, and logical execution time. Integrated into the Lingua Franca compiler and executed by the PretVM runtime, quasi-statically scheduled programs reduce average runtime overhead by 9× over dynamic scheduling while providing anomaly-free timing and analyzable worst-case makespan without requiring per-step worst-case execution times. An integration with Mocasin further enables compile-time design space exploration over time–energy trade-offs on heterogeneous platforms.

• A modernized implementation of GameTime, a timing analysis tool that combines game-theoretic online learning and systematic testing using satisfiability modulo theories (SMT) solvers. GameTime can estimate worst-case execution times of reaction bodies as well as answer other timing analysis questions. Rebuilt on LLVM and KLEE and supporting cycle-accurate emulation on FlexPRET, it supplies timing estimates for sequential programs consumed by the system-level and quasi-static analyses above, closing the loop between design-time reasoning and the actual execution-time behavior of generated code.

These contributions form a toolchain that connects analyzable CPS models, automated verification at the engineering level, and quasi-static scheduling into deterministic, verifiably correct, high-performing implementations.},
}

EndNote citation:

%0 Thesis
%A Lin, Shaokai 
%T Verifiable Cyber-Physical Systems: Building Engineering Models for Deterministic and Predictable Concurrent Execution
%I EECS Department, University of California, Berkeley
%D 2026
%8 May 19
%@ UCB/EECS-2026-211
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2026/EECS-2026-211.html
%F Lin:EECS-2026-211