IRIF, 8 place Aurélie Nemours (bâtiment Sophie Germain) dans le 13ème (RER C & ligne 14 : arrêt Bibliothèque François Mitterrand; Tram T3a : arrêt Avenue de France; Bus 62 & 89 : arrêt Porte de France).
Comme l’accès à l’IRIF est badgé, je propose de vous attendre en bas du bâtiment, je serai là dès 13:40. On montera au 3ème étage ensemble vers 13:55.
Abstract : 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) by a system; and φ is monitorable if it is violation or satisfaction monitorable. 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, i.e., where formulae can express both the order of events and the quantity of time separating them. In this work, we solve the monitorability problem for Tlin, a new expressive (linear-time) timed µ-calculus that we propose. First, we show that Tlin is strictly more expressive than MTL, the de facto timed extension of the well-known LTL. Second, we identify MTlin , the largest monitorable fragment of Tlin and characterise its largest subsets of formulae that are violation monitorable, satisfaction monitorable, and complete monitorable (both satisfaction and violation monitorable). To the best of our knowledge, this is the first work that solves the monitorability problem for such an expressive timed logic. Our theoretical results are accompanied with compilers (i) from MTL to Tlin and (ii) from MTlin formulae to monitors.
Abstract : Real-time systems (RTSs) are at the heart of numerous safety-critical applications. An RTS typically consists of a set of real-time tasks (the software) that execute on a multicore shared-memory platform (the hardware) following a scheduling policy. In an RTS, computing inter-core bounds, i.e., bounds separating events produced by tasks 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 ∈C) as a Uppaal timed automata (TA) network Nc. For each core c in C, Nc integrates blocking (due to data sharing) using tight analytical formulae. 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 TE ⊆T with different affinities CE ⊆C, requires model checking NE = ||c∈CE Nc, i.e., the parallel composition of all TA networks Nc for each c ∈CE, which produces a large, often intractable, state space. In this work, we present a new scalable approach based on (period-wise) exact abstractions to compute exact inter-core bounds in a schedulable RTS, under the assumption that tasks in TE have distinct affinities, i.e., |TE |= |CE |.We develop a novel algorithm, leveraging a new query that we implement in Uppaal, that computes for each TA network Nc in NE an abstraction A(Nc) preserving the exact intervals within which events occur on c. Then, we model check A(NE ) = ||c∈CE A(Nc) (instead of NE), therefore drastically reducing the state space. The scalability of our approach is demonstrated on the WATERS 2017 industrial challenge, for which we efficiently compute various types of inter-core bounds where FHZ fails to scale.
Abstract : 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.