Contract-based design is a promising design methodology that leverages rigorous specification, refinement relation, and composition operation for compositional reasoning to address system design complexity and heterogeneity by facilitating independent development of the subsystems. However, vacuous implementations-those with empty behaviors under the targeted environment-can occur even if the subsystem designers correctly refine the contracts according to the refinement relation. This compromises the benefits of independent development as vacuous implementations fail to satisfy the design goals. Although previous research emphasizes the importance of strong replaceability and receptiveness in addressing this issue, strong replaceability in feedback composition is not guaranteed. In this paper, we tackle this challenge by identifying conditions to ensure strong replaceability in feedback composition. These conditions are developed and validated through the analysis of fixed obligations, representing the behaviors collaboratively allowed by subsystem contracts, and fixed obligation graphs, which illustrate the relation between fixed obligations. We propose algorithms to verify strong replaceability for the subsystem contracts, offering a general approach that utilizes set operations and satisfiability modulo theories-based encoding to circumvent reliance on specific underlying theories in contract descriptions. By addressing this gap in contract-based design methodology, our developed conditions and algorithms ensure correct and meaningful implementations.
The future of automotive communication hinges on integrating legacy real-time protocols with advanced Ethernet technologies to empower Software-Defined Vehicles (SDVs). SDVs propose the adoption of the zonal computing architectures, which centralize vehicle functions into distinct zones connected by a high-speed communication backbone. While on the one hand, different zones can employ distinct network protocols like CAN, FlexRay, etc., Time Sensitive Ethernet (IEEE802.1Q) is being projected as the most promising protocol for the central backbone network. With such a heterogeneous distributed platform, SDVs demand reliable and deterministic end-to-end communication strategies, especially for zone-to-backbone or interzonal traffic via the central backbone. Although, there exist a few strategies for message transmission across heterogeneous network domains, they are ad-hoc in nature and oblivious to the precise demands of the control applications they cater to. These drawbacks may lead to poor bandwidth utilization and/or network congestion. Opposed to these ad-hoc techniques, this work proposes an optimal SMT (Satisfiability Modulo Theories) formulation for i) multiplexing periodic zonal message frames onto a minimum number of Ethernet frames, taking into account ($m, k$) -firmness-based relaxations on specific message flows, and ii) routing Ethernet frames between specified source and destination switches. Through extensive experimental evaluations of the proposed formulation using Z3 solver demonstrate substantial performance improvements, showing at least 30 % gain in frame utilization under diverse traffic conditions and timing constraints. Our results validate the proposed approach as a robust solution for ensuring efficient and predictable real-time communication in futuristic SDVs.
Certifying real-time guarantees for imperative programs is a critical challenge in embedded systems and cyber-physical applications. However, existing certified compilers lack the capability to accurately translate high-level timing abstractions into low-level executable code while preserving temporal semantics. This paper introduces a category-theoretic framework to model time-sensitive programs, leveraging monads and comonads to capture both the production and observation of temporal effects. Our methodology is formalized in the Rocq proof assistant, providing a foundation for the development of a certified compiler capable of preserving realtime constraints across compilation stages. By abstracting timing effects categorically, this work bridges the gap between theoretical program semantics and practical real-time certification, offering a principled path toward verified compilation for time-critical systems.
With the increasing availability of computational resources and the progress in research concerning automated formal methods, the characterization of safety features for hardware requires improved precision in functional vulnerability detection. In the context of formal fault injection, the model checking algorithm can be used to detect vulnerabilities in digital systems by violating the nominal temporal properties. We present a general methodology to reduce the state space that is computed and traversed during these fault campaigns. The chosen criteria preserves the nominal behavior and the failure modes, expressed by the fault-violated properties. This process is crucial to provide a manipulable object for subsequent Failure Mode and Effects Analysis. Finally, we propose an assumption-based guarantee technique to model how a fault may propagate through different hardware units, for a scalable methodology of formal fault injection and vulnerability detection in complex SoCs.
Machine Learning (ML) models are increasingly adopted in Cyber-Physical Systems (CPS), yet monolithic architectures hinder interpretability, verification, and safety assurance. By decomposing a CPS into modular sub-models and embedding formally defined safety policies during training, we can construct systems that are correct-by-construction rather than relying on post-hoc falsification or unscalable static verification. In this work, we introduce a policy-driven framework for compositional ML-based CPS. Using an autonomous vehicle as a representative case study, we show how to decompose a monolithic ML model into composable sub-models, mine meaningful safety properties from data, and use these policies to guide the training of each sub-model. To address unexpected or unseen scenarios where learned models may fail to comply with safety expectations, we employ a runtime enforcement mechanism that monitors model outputs and ensures policy adherence in real time. We test the approach through custom simulation of compositional designs, and through comparative analysis, we show how compositional property-based training and enforcement improve the safety of ML-based CPS.
I will report our recent work on model-based formal design of safety-critical embedded systems. With our approach, one can build a graphical model for a system to be developed with the combination of Simulink/Stateflow and AADL (AADL+S/S), and then conduct extensive simulation. Any AADL+S/S graphical model can be translated to an HCSP formal model automatically, so that the translated HCSP formal model can be verified using Hybrid Hoare Logic and its theorem prover. To justify the correctness of the translation, we define formal semantics of AADL+S/S and HCSP respectively with HUTP (Higher-order Unifying Theories of Programming), the correctness of the translation can therefore be proved theoretically. Finally, we propose the notion of approximate bisimulation for HCSP, and define a set of refinement rules through which we can refine an HCSP process into a piece of SystemC code or ANSI-C code, which is approximate bisimilar to the original HCSP process. All the above are supported by a tool chain called MARS. We applied the above approach to design some real-world case studies.
The paradigm of Logical Execution Time (LET) tasks is widely adopted by major tool vendors for designing deterministic and time-predictable software in multi-core systems, particularly in the automotive industry. To extend the use of LET in distributed environments, System Level Logical Execution Time (SL-LET) has been developed to effectively manage communication and delays between networked devices. However, there is currently a lack of open-source tools available for SL-LET, and the task allocation and scheduling problem for SL-LET remains unsolved. To address these concerns, we introduces a novel Integer Linear Programming (ILP)-based optimisation approach for SL-LET task allocation and scheduling, focusing on minimising core utilisation and average system response times. To illustrate the effectiveness of the approach, we benchmark our ILP-based solution against a traditional core allocation heuristic across multiple task sets. Through this evaluation, our approach, when compared to the heuristic, is able to demonstrate average response times that are 26.9% smaller.
The bittide system is a recent approach to distributed computing, designed to achieve synchronous execution at a large scale without the need for a global clock or traditional wall-clock synchronization. It aims to overcome the complexity and expense of maintaining precise wall-clock time in distributed systems, especially at datacenter scale. The underlying mechanism of bittide uses feedback control to regulate the frequency of the hardware oscillators driving both computation and communication, in such a way as to ensure that all nodes operate in syntony. This allows applications to treat time as purely logical, and to make use of deterministic scheduling and programming methodologies across the entire datacenter. In this talk we present an overview of the bittide system, discussing how the system works, mathematical formulations of the system behavior, and the consequences of logical synchrony for applications.
As Industry 4.0 drives the Fourth Industrial Revolution, Cyber-Physical Systems (CPSs) have become central to industrial automation. These systems integrate software with physical processes, significantly improving the efficiency and adaptability. However, this integration also expands the attack surface, exposing systems to Cyber-Physical-attacks (CP-attacks) that can target either the computational components, physical devices, or both. The impact of such attacks can be catastrophic, ranging from system disruption to physical damage. Although numerous techniques have been developed to detect and mitigate these threats, industrial standards are often not incorporated into the design of these methods. This limits their deployment within the Industry 4.0 systems, where standard compliance is critical. To this end, we extend IEC 61499, an emerging standard being considered in Industry 4.0, that uses reusable artefacts called function blocks. We formalise the mitigation of CP-attacks using a novel method based on Bi-directional Runtime Enforcement (Bi-RE) using a standards compliant approach called Secure Function Blocks (SFBs). This approach automatically generates the necessary enforcers from a timed specification language called Valued Discrete Timed Automaton (VDTA). We illustrate our approach using the case study of a water treatment system, and highlight the low overhead associated with it. This approach allows for runtime techniques to be applied with minimal changes to many Industry 4.0 applications.
Digital Twins (DTs) mimic a physical system using a digital version of the real system. While these have been explored in many domains, digital twins of human organs are yet to be created, especially those that are inspired by formal methods. To this end, we propose the first Cardiac Digital Twins (CDTs) by leveraging two key innovations from our research group. The first is a real-time model of the heart, that is based on a network of hybrid automata to represent the cardiac conduction system that mimics the rhythmic electrical activity of a normal heart. The model can be parametrised to exhibit disease states in real-time and this approach is being used by MathWorks for closedloop validation of pacemakers in real-time. This work has raised the interest of both device manufacturers and certification agencies, especially in the USA. Our group has expertise in digital biomarkers obtained from wearables, such as Electrocardiograms (ECGs) and Photoplethysmograms (PPGs). These provide a window into the cardiac cycle and we have already shown that the two signals are strongly correlated. Hence, a second innovation is related to using wearables to personalise the real-time heart model, so that the model generates ECGs matching that of an individual in different states. Our approach paves the way for developing personalised therapies, realtime monitoring, and accurate estimation of heart rate variability.
Energy efficiency is a key concern in circuit design. With the end of Dennard scaling, voltages no longer scale with transistor size, making full-capacity operation unsustainable due to heat and power limits. Power gating offers a solution, but controlling independent power domains is challenging. Large domains are manageable but inefficient; small domains are efficient but require intricate control. This paper introduces algorithms, integrated into a high-level synthesis tool, to automate fine-grained power domain partitioning and control. From a dataflow representation, the tool classifies actors into always-on and sleepable domains and generates wake signals. Experiments produced circuits with 48 to 541 power domains, many more than manually feasible, while ensuring correctness despite wake delays. Domains were asleep 60-73%; coordinating wake/sleep cycles for interdependent actors could increase runtime.
Contract-based component selection reduces design time and cost by encouraging the reuse of subsystem designs from an existing library. However, existing techniques assume the objective function is expressed solely with component parameters, such as size, cost, and power consumed, adding the burden of characterizing components with parameters and deriving the appropriate objective as a function of these parameters. We argue that this process does not consider behavior abstractions that could make the selection process more effective. We propose a contract-based component selection algorithm that consists of two parts: a contract-based system reasoning part that guides the selection and a black-box optimizer that selects the final choice. The contract-based systemreasoning part can evaluate, verify, and suggest the selection based on system behavior using contract operations to guide the blackbox optimizer. Experimental results based on the design problem for an unmanned aerial vehicle propulsion system, show that our proposed methods can successfully find and optimize component selection for all test cases within the time limit and outperform the existing methods.
Cryogenic power electronics has the potential to significantly improve Cyber Physical Systems (CPS) applications in aviation and space. However, their safety and reliability are yet to be studied systematically. To this end, we propose the first prototype of a deterministic toolchain for the design of Cryogenic Cyber Physical Systems (CCPS). Obviously, the design, verification and safety analysis of such systems pose considerable unknowns and challenges. Towards a potential solution, we propose an approach for unified functional safety, inspired by our earlier work. We leverage the recently developed deterministic framework (proposed by Google), called Logical Synchrony Networks, for distributed systems. This simplifies the modelling and safety analysis. Moreover, we propose a novel variant of Signal Temporal Logic (STL), called Synchronous Signal Temporal Logic (SSTL), which is specially tailored for CPS applications and designed using logical synchrony. We demonstrate the first prototype solution in the simulation of a CCPS system as a proof of concept.
Synchronous programs are used to implement safety critical embedded software. Efficiently compiling imperative synchronous programs into small and fast executables is challenging, due to state-space explosion. This paper introduces a novel linear time compilation technique for automata based compilation of synchronous programs. Graph based rewrite rules for kernel programming constructs are introduced. The compiled program is encoded into a type-state program using template meta-programming in C++. Experimental results show that the compilation time and generated binary size is comparable, while the execution times are on average 31-60% faster than current state-of-the-art compilers.
As multicore systems continue to scale, cache coherence has emerged as a critical determinant of system performance, with coherence behavior and task execution deeply intertwined-reshaping intertask dependencies. Task graph modeling offers a structured way to capture such dependencies and serves as the foundation for many system-level design strategies. However, these strategies typically rely on predefined task graphs, while many real-world applications lack explicit task graphs and exhibit dynamic, data-dependent behavior, limiting the effectiveness of static approaches. Thus, many task graph modeling methods for realistic workloads have been developed. However, they either rely on implicit methods-using application-specific features without producing explicit graphs-or generate graphs tailored to fixed scheduling models, offering limited generality. Critically, they overlook coherence interactions, resulting in a mismatch between design assumptions and actual runtime behavior. To address these limitations, we propose CoTAM, a Coherence-Aware Task Graph Modeling framework for realistic workloads that constructs a unified task graph reflecting runtime behavior. CoTAM analyzes the impact of coherence by decoupling its behavior from overall execution. It then quantifies the influence of coherence through a learned weighting scheme, infers inter-task dependencies for coherence-aware task graph generation. Extensive experiments demonstrate the superiority of CoTAM over implicit methods, not only bridging the gap between dynamic workload behavior and existing designs, but also underscoring the importance of incorporating cache coherence into task graph modeling for accurate and generalizable system-level analysis.
Hyperproperties for Time Window Temporal Logic (HyperTWTL) is a domain-specific formal specification language known for its effectiveness in compactly representing security, opacity, and concurrency properties for robotics applications. This paper focuses on HyperTWTL-constrained secure reinforcement learning (SecRL). Although temporal logic-constrained safe reinforcement learning (SRL) is an evolving research problem with several existing literature, there is a significant research gap in exploring security-aware reinforcement learning (RL) using hyperproperties. Given the dynamics of an agent as a Markov Decision Process (MDP) and opacity/security constraints formalized as HyperTWTL, we propose an approach for learning security-aware optimal policies using dynamic Boltzmann softmax RL while satisfying the HyperTWTL constraints. The effectiveness and scalability of our proposed approach are demonstrated using a pick-up and delivery robotic mission case study. We also compare our results with two other baseline RL algorithms, showing that our proposed method outperforms them.
The design of complex cyber-physical systems involves balancing multiple, often conflicting performance objectives. In practice, some design requirements remain implicit, embedded in the intuition and expertise of seasoned designers who have worked on similar systems for years. These designers rely on their experience to explore a limited set of promising design candidates, evaluating or simulating them with detailed but computationally slow scientific models. The typical goal is to produce a diverse array of high-performing configurations that offer flexibility in trade-offs and avoid premature commitment to a specific design. In this invited talk, we describe an AI assistant that leverages neuro-symbolic machine learning to automate parts of the system design process. Our approach extends oracle-guided inductive synthesis by integrating a hierarchy of oracles, ranging from slow, detailed scientific models to faster but lower-fidelity deep neural network surrogates and symbolic rules. This approach accelerates design iterations, especially during early design phases. We employ deep generative models in the form of fine-tuned large language models to learn the valid design space, followed by joint exploration and optimization across this learned manifold. This allows the generation of a diverse set of optimal designs based on specified performance objectives.
In this paper, we perform a safety and performance analysis of an autonomous vehicle utilizing a reactive planner and controller to navigate a race lap. Unlike traditional planning algorithms that use a map of the environment, the reactive planner generates the plan based solely on current sensor inputs. Our reactive planner selects a waypoint on the local Voronoi diagram, and we use a pure-pursuit controller to navigate towards this waypoint.Our analysis consists of two parts. The first part demonstrates that the reactive planner computes a plan locally consistent with the Voronoi plan derived from a full map. The second part models the vehicle’s navigation along the Voronoi diagram as a hybrid automaton. To prove the safety and performance specifications, we compute the reachable set of this hybrid automaton and apply enhancements to simplify this computation. We show that an autonomous vehicle using our reactive planner and controller is safe and successfully completes a lap on five different circuits. Additionally, we have implemented our planner and controller in a simulation environment and on a scaled-down autonomous vehicle, demonstrating that our approach works well across a variety of circuits.
Dataflow networks play a vital role in modeling and analyzing stream-processing systems in an analytic way, including digital signal and image processing systems. In this paper, we first present a system-level approach to synthesize such dataflow networks automatically to systems of communicating hardware actors connected by FIFO buffers. Although such data-triggered networks of (internally clocked) actors can achieve very high throughputs, the potential to power actors down in times of unavailability of data has not been addressed so far in any research. Here, we show that by refinement of the firing state machine of each actor in a given network, we enable the design of self-powering dataflow networks while exploiting either clock gating or power gating as a means to save power in times of inactivity of each individual actor in a network. The gains of self-powering dataflow networks in terms of power and energy savings when powering down and up actors dynamically is shown for different data arrival patterns and rates in detailed experiments for multiple IoT system applications. These systems are often working in normally-off mode and woken up only upon the availability of data. For these, drastic energy savings are reported.
Determinacy is a desirable but difficult-to-achieve behavioural property in scalable distributed systems. Deterministic Models of Computation range from the asynchronous Kahn Process Networks to synchronous reactive languages such as Lustre, where logical clocks enforce the synchrony hypothesis. These models have well-founded data-flow s emantics w here computations are viewed as the least fixed point solutions of simultaneous equations defined by continuous functions on streams of discrete values. However, scalable and efficient implementations of the Kahn model are challenging to construct, while the synchrony hypothesis in Lustre makes distributed implementations difficult. Moreover, determinacy is a consequence of specific assumptions built into the computational model. The notion of Logical Synchrony, proposed by Lall et al., and explored further by Kenwright et al., suggests that synchronisation issues may be decoupled from computation, leading to a distributed model where computations at independent nodes are related by invariant logical delays. We provide a semantic notion of behaviour for functional processes running on such Logical Synchrony Networks (extension graphs), and an appropriate and robust notion of logical observational equivalence (wavefront equivalence) retaining semantic aspects of KPNs, specifically determinacy. Further, we propose extending the versatile notion of the synchronous observer, exploited in the Lustre toolset, to a network of located synchronous observers with the same invariant logical delays as the distributed system. Thus we will be able to use the same logically synchronous model of computation for checking or monitoring a class of (safety) properties of programs, specifying axioms and assumptions on behaviour, constraining models and specifying test cases, etc.
