Abstract: MIMOS is a tool environment for the design, simulation, verification, scheduling, and code generation of embedded real-time systems on heterogeneous multi-core platforms. MIMOS primarily targets safety-critical applications, where correct functional and timing behaviors are essential. The MIMOS tools provide a seamless approach to safe system development, ensuring that specified functionalities and timing behaviors specified and verified during the design phase are faithfully realized in the final implementation. This allows for customizable embedded real-time systems, enabling modifications to the design model without touching the executables in the final implementation.

Unlike existing tools such as Simulink and SCADE, which are all rooted in the synchronous design paradigms, MIMOS employs an asynchronous yet deterministic semantics model. This model is designed to not only guarantee (1) determinism but also facilitate (2) composability throughout all design stages, from system modeling to final implementation. This allows for dynamic updates for systems in operation. Furthermore, the asynchronous semantics of MIMOS enables pipelined parallel computation for (3) optimal performance with respects to both end-to-end latency and system throughput.

Essentially, a MIMOS model consists of a network of independent components that communicate through two types of channels: FIFO queues and registers. The FIFO queues are designed to support both non-blocking reads where no data is also considered an input, and non-blocking write operations. In contrast, a register is a single-capacity storage location that allows non-blocking read and write operations, overwriting its previous value with any new incoming data. Unlike FIFO queues, the contents of a register remain unchanged after a read operation. More precisely, a MIMOS model is a timed Kahn Process Network (KPN), where each node represents a periodic real-time task computing a mathematical function at a given rate. At the beginning of each period, the task reads its inputs; if the required inputs are available, it must compute the function before the period ends (ensured through schedulability analysis) and deliver the output by the end of the period or at a predetermined time point, such as the worst-case response time. If no inputs are available on the input channels when the period starts, essentially no computation is required. Thanks to the periodic timing behavior of reading, computation, and writing at each node, we can demonstrate that the non-blocking reading of inputs from both registers and FIFO channels is equivalent to a function over timed streams. Consequently, the MIMOS model operates under deterministic timed semantics.

Abstract: Program verification often relies on human experts to write a significant amount of auxiliary specifications, such as function contracts and loop invariants, hindering its wider applications in real-world projects. To help alleviate this practical challenge, we present in this talk, AutoSpec, an automated approach to generating specifications with LLM for automated program verification. AutoSpec overcomes the shortcomings of existing work in specification versatility by synthesizing satisfiable and adequate specifications for proof completeness. It leverages the power of LLM, static analysis and program verification. We will also share some of our ongoing efforts aiming to further improve the performance of LLM-driven program specification generation.

Abstract: We study a variant of the problem of synthesizing Mealy machines that enforce LTL specifications against a hostile environment. In this variant, the user provides the high-level LTL specification \(\varphi\) of the system to be designed, along with a set \(E\) of example executions that the solution must produce. Our synthesis algorithm operates in two phases. First, it generalizes the decisions made along the examples in \(E\), using tailored extensions of automata learning algorithms. This phase ensures that the user-provided examples in \(E\) are generalized while maintaining the realizability of \(\varphi\). Second, the algorithm converts the (typically) incomplete Mealy machine obtained from the learning phase into a complete Mealy machine that realizes \(\varphi\). The examples are used to guide the synthesis process.

We provide a completeness result, demonstrating that our procedure can learn any Mealy machine \(M\) that realizes \(\varphi\) with a small (polynomial-sized) set of examples. Furthermore, we show that our problem, which generalizes the classical LTL synthesis problem (i.e., when \(E = \emptyset\)), retains the same worst-case complexity. The additional cost of learning from \(E\) is polynomial in both the size of \(E\) and the size of a symbolic representation of solutions that realize \(\varphi\).

Additionally, we show how this framework can be applied when the reactive system to be synthesized interacts with an oblivious stochastic environment that can be sampled. In this case, we present an algorithm capable of producing complete examples from samples of the environment's behavior, optimized according to a reward function provided to the synthesis procedure. These examples are then incorporated into the synthesis procedure described above.