Abstract Quantitative monitoring mitigates two issues observed in exhaustive, qualitative verification approaches, namely the state-space explosion problem and the rigidity of their binary verdicts. This is achieved through (i) analysing individual executions instead of building the whole state-space and (ii) providing a robustness measure instead of yes/no answers. In this paper, we consider real-time systems where executions and specifications are modelled as timed signals and Signal Temporal Logic (STL) formulae, respectively. We propose a new temporal robustness measure $\delta $ δ for STL, based on a new distance that we define over timed signals. In contrast with existing measures, $\delta $ δ provides a precise quantification of distances between the monitored signal and the boundary separating faulty and non-faulty executions w.r.t. an STL property. Thus, $\delta $ δ is suitable for a wide range of real-life perturbations, such as those affecting exclusively a particular time window within a signal. Though we prove that computing $\delta $ δ is NP-hard in general, we provide efficient algorithms for a practical fragment of STL. In particular, this fragment includes the key property of bounded response. This paper is an extension of (Rino et al. in Joint International Conference on Quantitative Evaluation of SysTems & International Conference on Formal Modeling and Analysis of Timed Systems (QEST+FORMATS), 2024), published at QEST+FORMATS 2024. The extension includes implementation of algorithms to compute $\delta $ δ in a prototype tool, and an evaluation of our approach on a case study of quality assessment of insulin controllers for diabetic patients.

Runtime Verification (RV) is gaining popularity due to its scalability and ability to analyse block-box systems. Monitoring is at the heart of RV; a logical formula ϕ, formalising some property of interest, is typically translated into a monitor that checks whether the system under scrutiny satisfies ϕ during its execution. A logical formula ϕ is violation (resp. satisfaction) monitorable iff there exists a monitor for ϕ that is both sound and complete w.r.t. its violation (resp. satisfaction). The monitorability problem is thus concerned with determining the largest subset of a logic L that is monitorable. Although this problem has been solved for expressive untimed logics, it remains open for timed logics, where formulae can express both the order of events and the quantity of time separating them. This paper solves the monitorability problem for T^lin, a new expressive (linear-time) timed μ-calculus that we propose. First, we show that T^lin is strictly more expressive than MTL, the de facto timed extension of LTL. Second, we identify MT^lin, the largest monitorable fragment of T^lin: we characterise its largest subsets of formulae that are violation monitorable, satisfaction monitorable, and complete monitorable (both satisfaction and violation monitorable). To wit, this is the first work that answers the monitorability question for such an expressive timed logic.

In recent years, many different methods for identifying hybrid automata from data have been proposed. However, most of these methods consider clean simulator data, and consequently do not perform well for noisy data measured from real systems. We address this shortcoming with a new approach for the identification of hybrid automata that is specifically designed to be robust to noise. In particular, we propose a new high-level strategy consisting of the following three steps: clustering based on the dynamics identified from a local dataset, state space partitioning using decision trees, and conversion of the decision tree to a hybrid automaton. In addition, we introduce several new concepts for the realization of the single steps. For example, we propose an automated regularization of the dynamic models used for clustering via rank adaption, as well as a new variant of the Gini impurity index for decision tree learning, tailored toward hybrid systems where different dynamics can be active within the same state space region. As our experiments on 19 challenging benchmarks with different characteristics demonstrate, in addition to being robust to both process and measurement noise, our approach avoids the need for extensive hyper-parameter tuning and also performs well for clean data without noise.

A real-time systems (RTS) typically consists of a set of real-time tasks that execute on a multicore platform following a scheduling policy. In an RTS, computing inter-core bounds, i.e., bounds separating events occurring on different cores, is crucial. While efficient techniques to over-approximate such bounds exist, little has been proposed to compute their exact values. Given an RTS with a set of cores$c$and a set of tasks$T$, under partitioned fixed-priority scheduling with limited preemption, a recent work by Foughali, Hladik and Zuepke (FHZ) models tasks with affinity$c$(i.e., allocated to core$c\in C$) as a Uppaaltimed automata (TA) network$N_{C}$. Through compositional model checking, FHZ achieved a substantial gain in scalability for bounds local to a core. However, computing inter-core bounds for some events of interest$E$, produced by a subset of tasks$T_{E}\subseteq T$with different affinities$C_{E}\subseteq C$, requires model checking$N_{E}=\Vert _{c\in C_{E}}N_{c}$, i.e., the parallel composition of all TA networks$N_{c}$for each$c\in C_{E}$, which often produces an intractable state space. In this paper, we present a new scalable approach based on exact abstractions to compute exact inter-core bounds in a schedulable RTS, under the assumption that tasks in$T_{E}$have distinct affinities. We develop a new Uppaalquery, and a novel algorithm that computes, for each TA network$N_{c}$in$N_{1\mathrm{i}}$, an abstraction$\mathcal{A}(N_{c})$preserving the exact intervals within which events occur on$c$. Then, we model check$\mathcal{A}(N_{E})=\Vert _{c\in C_{E}}\mathcal{A}(N_{c})$(instead of$N_{E}$), therefore drastically reducing the state space. We demonstrate the scalability of our approach as we efficiently compute inter-core bounds for the WATERS 2017 industrial challenge, where FHZ fails to scale.

In an embedded real-time system (ERTS), real-time tasks (software) are typically executed on a multicore shared-memory platform (hardware). The number of cores is usually small, contrasted with a larger number of complex tasks that share data to collaborate. Since most ERTSs are safety-critical, it is crucial to rigorously verify their software against various real-time requirements under the actual hardware constraints (concurrent access to data, number of cores). Both the real-time systems and the formal methods communities provide elegant techniques to realize such verification, which nevertheless face major challenges. For instance, model checking (formal methods) suffers from the state-space explosion problem, whereas schedulability analysis (real-time systems) is pessimistic and restricted to simple task models and schedulability properties. In this paper, we propose a scalable and generic approach to formally verify ERTSs. The core contribution is enabling, through joining the forces of both communities, compositional verification to tame the state-space size. To that end, we formalize a realistic ERTS model where tasks are complex with an arbitrary number of jobs and job segments, then show that compositional verification of such model is possible, using a hybrid approach (from both communities), under the state-of-the-art partitioned fixed-priority (P-FP) with limited preemption scheduling algorithm. The approach consists of the following steps, given the above ERTS model and scheduling algorithm. First, we compute fine-grained data sharing overheads for each job segment that reads or writes some data from the shared memory. Second, we generalize an algorithm that, aware of the data sharing overheads, computes an affinity (task-core allocation) guaranteeing the schedulability of hard-real-time (HRT) tasks. Third, we devise a timed automata (TA) model of the ERTS, that takes into account the affinity, the data sharing overheads and the scheduling algorithm, on which we demonstrate that various properties can be verified compositionally, i.e., on a subset of cores instead of the whole ERTS, therefore reducing the state-space size. In particular, we enable the scalable computation of tight worst-case response times (WCRTs) and other tight bounds separating events on different cores, thus overcoming the pessimism of schedulability analysis techniques. We fully automate our approach and show its benefits on three real-world complex ERTSs, namely two autonomous robots and an automotive case study from the WATERS 2017 industrial challenge.

Throughout the last few decades, researchers and practitioners are showing more and more interest in using formal methods in order to predict and prevent software failures in robotic and autonomous systems. However, the applicability of formal methods to such systems is limited due to several factors. For instance, robotic specifications are often non-formal which makes their formalization hard and error prone, and their translation into formal models ad-hoc and non automatic. Furthermore, the complexity and size of robotic applications lead most often to scalability issues with exhaustive techniques such as model checking. In this paper, we investigate the use of runtime verification as an alternative to model checking for the rigorous verification of large robotic systems. To do so, we first develop a sound and automatic translation from the robotic framework GenoM3 to the real-time version of the BIP formal language. Then, we apply the translation to a real-world case study the formal models of which do not scale with model checking, and use the BIP Engine to execute the generated BIP model, verify properties online, and adequately react to their possible violation. The experiments are carried out on a real Robotnik robot and show the efficiency of our approach in verifying timed properties, that is when the amount of time separating events is important.

Due to the severe consequences of their possible failure, robotic systems must be rigorously verified against (i) behavioral properties, such as safety and (ii) real-time properties, such as schedulability, while taking into account the real hardware (e.g. number of cores) and operating system (e.g. scheduling policy) specificities. Formal verification and schedulability analysis are popular approaches that may help with such verification, but suffer from limitations such as scalability issues (for the former) and difficulty to generalize to complex robotic tasks (for the latter), when used independently. In this paper, we propose a two-step, efficient solution that combines both approaches. The first step provides a sufficient condition for the schedulability of hard-real-time tasks in a robotic application. Then, the second step automatically generates a formal model of the application, on which other important properties may be verified formally using statistical model checking. The solution is applied to an autonomous drone case study.

Simulation is very helpful for the development of cyber-physical systems, as it enables testing functionalities and their integration without full hardware deployment. For complex systems, such as fleets of heterogeneous robots, multiple simulators dedicated to particular physical processes must be interconnected, so as to build a wholesome simulation and test the overall system. A key property to ensure is that the overall simulation is repeatable. We propose a lightweight distributed architecture for time management, allowing to easily deploy complex simulations while strictly ensuring repeatability. A formal model of the architecture is provided, along with a proof of progress. An open source implementation, with a binding to the robotic ROS framework is made available.