International audience

Opacity is an essential feature in the control and supervision of cyberphysical systems, in particular w.r.t. cybersecurity. It prevents intruders from knowing whether the system accessed specific secret states. In particular, a quantified variant of the opacity property, called K-step opacity, ensures that the intruder cannot determine the passage of the system through a secret state within K steps following such a passage. This paper introduces an algebraic method to verify K-step opacity in discrete event systems modeled by partially observed labeled Petri nets. Namely, we develop an algebraic formulation that establishes a necessary and sufficient condition for K-step opacity, and sets the basis for investigating this feature by means of optimization techniques. The underlying idea is to eliminate the need to build the state space of the net or any derived graph, thus tackling the potentially related combinatorial explosion problem.

Neural networks as a machine learning technique are increasingly deployed in various domains. Despite their performance and their continuous improvement, the deployment of neural networks in safety-critical systems, in particular for autonomous mobility, remains restricted. This is mainly due to the lack of (formal) specifications and verification methods and tools that allow for having sufficient confidence in the behavior of the neural-network-based functions. Recent years have seen neural network verification getting more attention; many verification methods were proposed, yet the practical applicability of these methods to real-world neural network models remains limited. The main challenge of neural network verification methods is related to the computational complexity and the large size of neural networks pertaining to complex functions. As a consequence, applying abstraction methods for neural network verification purposes is seen as a promising mean to cope with such issues. The aim of abstraction is to build an abstract model by omitting some irrelevant details or some details that are not highly impacting w.r.t some considered features. Thus, the verification process is made faster and easier while preserving, to some extent, the relevant behavior regarding the properties to be examined on the original model. In this article, we review both the abstraction techniques for activation functions and model size reduction approaches, with a particular focus on the latter. The review primarily discusses the application of abstraction techniques on feed-forward neural networks and explores the potential for applying abstraction to other types of neural networks. Throughout the article, we present the main idea of each approach and then discuss its respective advantages and limitations in detail. Finally, we provide some insights and guidelines to improve the discussed methods.

Although Unified Modeling Language (UML) state machines constitute a convenient modeling formalism that is widely used in many applications, the lack of formal semantics impedes carrying out automatic processing, such as formal verification. In this article, we aim to achieve a proven translation from a subset of UML state machines to timed automata. A generic abstract syntax is defined for state machines that allows us to specify state machines as a tree-like structure, explicitly illustrating the hierarchical relationships within the model. Based on this syntax, a formal asynchronous semantics for state machines and systems of state machines is established. Additionally, the semantics of timed automata is specified. Then, a translation relation from the considered set of state machines to timed automata is defined and a strong equivalence relation — namely, a timed bisimulation between the source and target models — is formally proven. The proof is carried out inductively while considering continuous (time) and discrete transitions separately. This proof allows us to demonstrate a strong similitude between these models.

Neural networks (NNs) have witnessed widespread deployment across various domains, including some safetycritical applications. In this regard, the demand for verifying means of such artificial intelligence techniques is more and more pressing. Nowadays, the development of evaluation approaches for NNs is a hot topic that is attracting considerable interest, and a number of verification methods have been proposed. Yet, a challenging issue for NN verification is pertaining to the scalability when some NNs of practical interest have to be evaluated. This work aims to present INNAbstract, an abstraction method to reduce the size of NNs, which leads to improving the scalability of NN verification and reachability analysis methods. This is achieved by merging neurons while ensuring that the obtained model (i.e., abstract model) overapproximates the original one. INNAbstract supports networks with numerous activation functions. In addition, we propose a heuristic for nodes' selection to build more precise abstract models, in the sense that the outputs are closer to those of the original network. The experimental results illustrate the efficiency of the proposed approach compared to the existing relevant abstraction techniques. Furthermore, they demonstrate that INNAbstract can help the existing verification tools to be applied on larger networks while considering various activation functions.

Diagnosability of faults in discrete event systems modeled with Petri nets can be assessed either via graph-based techniques (also called diagnoser, verifier/twin-plant based techniques), or via the solution of optimization problems. The approaches that belong to the former class are based on the analysis of the net reachability or coverability graphs (or of a more compact version of them). The latter approach exploits the mathematical representation of the net itself to specify and solve optimization problems, which are usually expressed as integer linear programming (ILP) problems. In this paper we exploit the railway Petri net model originally proposed in [16], and extended in [14] to be used as a benchmark for diagnosability analysis, to assess the efficiency of the approach based on the solution of ILP problems proposed in [3]. In order to show the effectiveness of the proposed technique, a comparison with a graph-based approach for analyzing diagnosability is also presented.

This paper deals with a benchmark-based experimental comparison of three diagnoser-based approaches for fault diagnosis of discrete event systems modeled by Petri nets: the MBRG/BRD approach, the FMG/FMSG approach and the SSD approach. The experiments are performed on a level crossing benchmark, using the respective software tools integrating the approaches. Different features are shown in terms of state-space building (exhaustive or partial), procedure for analyzing diagnosability (based on complete or on-the-fly built state-space) and state-space representation (concrete or symbolic). Based on the obtained experimental results, a comparative discussion is provided particularly regarding memory and time consumption for analyzing diagnosability of the three techniques.

Level crossing (LC) safety is a crucial issue for railway operators and infrastructure managers. Accidents at LCs give rise to serious material and human damage, while seriously impacting the reputation of railway safety. In particular, some typical scenarios are behind the main part of train-car collisions, which occur at LCs. On the other hand, European Rail Traffic Management System (ERTMS) is the standard railway control-command and signaling system that is currently being implemented throughout Europe and elsewhere. The aim is to ensure railway interoperability while enhancing safety and competitiveness of the railway transportation. ERTMS specifications only provide a rough description when dealing with LC control. This paper elaborates on a functional control architecture for automatic LCs in the context of ERTMS operation Levels 2 and 3. Indeed, these operation levels ensure a continuous knowledge of train location thanks to the Global System for Mobile Communications-Railways link between the trains and the Radio Block Center. Hence, the established LC control scheme aims to ensure an optimal LC command based on the information regarding the train location and, thereby, prevent some potential risky scenarios and improve the global safety at LCs. To achieve this, a generic methodology is employed. First, a formal behavioral model is developed using the time Petri net (TPN) notation. Then, the problem is formalized on the basis of the established TPN, in such a way as to carry out a sound and trustworthy analysis. The various steps of the developed approach are detailed and illustrated in the course of this paper. To the best of our knowledge, this is the first work that seeks to elaborate a control strategy of automatic LC in the ERTMS operation context.

As is witnessed by railway statistics, level crossing (LC) safety has always been one of the major concerns for railway stakeholders. LC safety is an issue at the crossroads between technical aspects, operational procedures, and human factors, making the search for effective solutions a challenging task. This paper deals with technical aspects related to LC safety. In particular, we carry out an analysis pertaining to the diagnosability of two main failure classes that can affect the protection system at automatic LCs. In this paper, a labeled Petri net behavioral model depicting the global system function, including both the normal operation and the faulty behavior, is first established. Petri net has been used as the modeling formalism mainly for its mathematical foundations and expressiveness capabilities. Using such a mathematical notation is highly recommended to deal with dependability issues in safety-critical systems, particularly in railways. Based on the established model, different model-based approaches for the diagnosis of discrete event systems (DESs) will be brought into play to investigate the diagnosability of two considered failure classes, whereas the obtained results will be compared. In particular, a technique that we have established, which is based on on-the-fly and incremental analysis of the model state space, shows interesting efficiency, making it possible to tackle the combinatorial explosion problem, which arises particularly when considering multi-track LCs. The originality of this technique w.r.t. existing DES model-based diagnosis approaches is that, in general, a partial building/investigation of the state space suffices to decide diagnosability and build an online diagnoser. Findings pertaining to LC safety are drawn based on a thorough discussion of the obtained results. In particular, we show how the diagnosability analysis outputs can be taken into account in the global LC risk assessment process.

Safety is a key issue in railway operation. In this context, level crossings (LCs) are one of the most critical points in railway networks. In some countries, accidents at LC account for up to 50% of railway accidents. In this paper, we conduct a risk assessment comparative study involving two main types of Automatic Protection Systems (APSs), the first using a pair of half-barriers and the second with four half-barriers. So far, the choice of such LC protection systems has been exclusively done on the basis of qualitative expertise. The study we carry out here is based on some parameterizable behavioral models we have developed, which describe the global dynamics within the LC area. In contrast to existing studies on LC safety, our models take into account not only railway and road traffic but also the risk due to human factors while focusing on two major risky situations. The simulation results clearly show the potential risk with each of the investigated APSs, according to various features of the dynamics within the LC area. To the best of our knowledge, this is the first work dealing with a quantitative comparison between different types of LCs. The developed models can be easily accommodated in order to describe existing infrastructures.

Level crossings (LCs) are considered to be a safety black spot for railway transportation since LC accidents/incidents dominate the railway accident landscape in Europe, thus considerably damaging the reputation of railway transportation. LC accidents cause more than 300 fatalities every year throughout Europe, which represents up to 50% of all deaths for railways. That is why LC safety is a major concern for railway stakeholders in particular and transportation authorities in general. LCs with an important traffic moment$^{1}$are generally equipped with automatic protection systems (APSs). Here, we focus on two main risky situations, which have caused several accidents at LCs. The first is the short opening duration between successive closure cycles relative to trains passing in opposite directions. The second is the long LC closure duration relative to slow trains. In this paper, we suggest a new APS architecture that prevents these kinds of scenarios and therefore increases the global safety of LCs. To validate the new architecture, a method based on well-formalized means has been developed, allowing us to obtain sound and trustworthy results. Our method uses a formal notation, i.e., timed automata (TA), for the specification phase and the model-checking formal technique for the verification process. All the steps are progressively discussed and illustrated.

Level crossings (LCs) are identified as critical security points in both road and rail infrastructures. Statistics show that more than 300 people are killed every year in Europe in more than 1200 accidents occurring at LCs. In this paper, we first propose a global model involving both rail and road traffic in the LC area. This model is obtained by a progressive integration of elementary models that we developed, each of which describes the behavior of a part in the whole LC environment. We are more precisely interested in a particular phenomenon that may cause collisions at LCs and corresponds to the accumulation of vehicles' waiting queues at the LC exit zone. As a notation, we use stochastic Petri nets (SPNs) in such a way as to precisely reflect the system's dynamics. Second, the simulation of the global system behavior is performed in light of the behavioral model while adopting the Monte Carlo principle. The TimeNet tool is used as a simulator that allows the monitoring of risky situations. To qualitatively and quantitatively assess the effect of various factors on the risk level, setup tasks are undertaken. Finally, the simulation results are analyzed and interpreted. This analysis makes it possible to consider some solutions to reduce the incurred risk.