Concentration inequalities are standard lemmas providing upper bounds on deviations of random variables. To formalize concentration inequalities, we have been developing a general library of lemmas for probability theory in the Rocq prover. This effort led us to revisit already established technical aspects of the Mathematical Components libraries. In this paper, we report on improvements of general interest resulting from our formalization. We devise types for numeric values and a lightweight semi-decision procedure, based on interval arithmetic. We also extend the hierarchy of available mathematical structures to formalize Lebesgue spaces. We illustrate our new formalization of probability theory with the complete proof of a concentration inequality for Bernoulli sampling.

Estimating the worst-case deadline failure probability (WCDFP) of a real-time task is notoriously difficult, primarily because a task's execution time typically depends on prior activations (i.e., history dependence) and the execution of other tasks (e.g., via shared inputs). Previous analyses have either assumed that execution times are probabilistically independent (which is unrealistic and unsafe), or relied on complex upper-bounding abstractions such as probabilistic worst-case execution time (pWCET), which mask dependencies with pessimism. Exploring an analytically novel direction, this paper proposes the first closed-form upper bound on WCDFP that accounts for dependent execution times. The proposed correlation-tolerant analysis (CTA), based on Cantelli's inequality, targets fixed-priority scheduling and requires only two basic summary statistics of each task's ground- truth execution time distribution: upper bounds on the mean and standard deviation (for any possible job-arrival sequence). Notably, CTA does not use pWCET, nor does it require the full execution-time distribution to be known. Core parts of the analysis have been verified with the Coq proof assistant. Empirical comparison with state-of-the-art WCDFP analyses reveals that CTA can yield significantly improved bounds (e.g., a lower WCDFP than any pWCET-based method for ~70% of the workloads tested at 90% pWCET utilization and 60% average utilization). Beyond accuracy gains, the favorable results highlight the potential of the previously unexplored analytical direction underlying CTA.

Computing response times for resources shared by periodic workloads (tasks or data flows) can be very time consuming as it depends on the least common multiple of the periods. In a previous study, a quadratic algorithm was provided to upper bound the response time of a set of periodic tasks with a fixed-priority scheduling. This paper generalises this result by considering a rate-latency server and sporadic workloads and gives a response time and residual curve that can be used in other contexts. It also provides a formal proof in the Coq language.

Some mathematical proofs involve intensive computations, for instance: the four-color theorem, Hales' theorem on sphere packing (formerly known as the Kepler conjecture) or interval arithmetic. For numerical computations, floating-point arithmetic enjoys widespread usage thanks to its efficiency, despite the introduction of rounding errors. Formal guarantees can be obtained on floating-point algorithms based on the IEEE 754 standard, which precisely specifies floating-point arithmetic and its rounding modes, and a proof assistant such as Coq, that enjoys efficient computation capabilities. Coq offers machine integers, however floating-point arithmetic still needed to be emulated using these integers. A modified version of Coq is presented that enables using the machine floating-point operators. The main obstacles to such an implementation and its soundness are discussed. Benchmarks show potential performance gains of two orders of magnitude.

In this paper, we outline a methodology allowing to support the formal verification of functional properties for generated code. When relying on a code generator, a model is directly mapped into the target embedded code, in C for instance. At model level, a specification can be associated to the model and used to assess the validity of the model with respect to its requirements. At code level, other means such as deductive methods can be used to ensure similar goals. While the analysis of user-specified properties at model-level is developed and tractable, the automatic verification of these specification at code level remains an open issue. We present here a framework which builds a semantics layer connecting model specification to code specification, as well as associated proof evidences. This approach has been designed and developed in the context of dataflow languages such as Simulink, SCADE or Lustre, typically used in the design of cyber-physical system controllers, but it could also be revisited in other contexts. The model is analyzed by SMT-based model checking and convex optimization-based static analysis. At code level, deductive techniques, such as implemented in Frama-C, are used to prove the functional correctness. Our approach combines static analysis with refinement to drive the proof at code level, relying on analysis results obtained at model level. The refinement relates the initial model semantics with the one of the code. This papers only outlines the methodology combining analyses. It has been applied manually on some examples. A fully implementation remains a future work.

Polynomial positivity over the real field is known to be decidable but even the best algorithms remain costly. An incomplete but often efficient alternative consists in looking for positivity witnesses as sum of squares decompositions. Such decompositions can in practice be obtained through convex optimization. Unfortunately, these methods only yield approximate solutions. Hence the need for formal verification of such witnesses. State of the art methods rely on heuristic roundings to exact solutions in the rational field. These solutions are then easy to verify in a proof assistant. However, this verification often turns out to be very costly, as rational coefficients may blow up during computations.

Network calculus (also known as real-time calculus) and event stream theory are two theories designed to compute upper bounds on response time for real-time systems. Both generalise the common periodic request arrival to any kind of workload using cumulative functions. In network calculus, a data flow is modelled by its cumulative curve, A(t), representing the amount of data sent by the flow up to time t, whereas the event stream theory counts the number of packets sent up to t, denoted by E(t). Of course, the size of packets is a link between both functions. This work presents a formal model embedding both A, E, the packet function, and their basic relations.

Robustness analyses play a major role in the synthesis and analysis of controllers. For control systems, robustness is a measure of the maximum tolerable model inaccuracies or perturbations that do not destabilize the system. Analyzing the robustness of a closed-loop system can be performed with multiple approaches: gain and phase margin computation for single-input single-output (SISO) linear systems, mu analysis, IQC computations, etc. However, none of these techniques consider the actual code in their analyses.

Recent work addressing the stability analysis of controllers at code level has been mainly focused on the controller alone. However, most of the properties of interest of control software lie in how they interact with their environment. We introduce an extension of the analysis framework to reason on the stability of closed loop systems, i.e., controllers along with a model of their physical environment, the plant. The proposed approach focuses on the closed loop stability of discrete linear control systems with saturations, interacting with a discrete linear plant. The analysis is performed in the state space domain using Lyapunov-based quadratic invariants. We specifically address the automatic synthesis of such invariants and the treatment of floating-point imprecision.

Embedded system control often relies on linear systems, which admit quadratic invariants. The parts of the code that host linear system implementations need dedicated analysis tools, since intervals or linear abstract domains will give imprecise results, if any at all, on these systems. Previous work by FERET proposes a specific abstraction for digital filters that addresses this issue on a specific class of controllers.