Search

First-Order Linear Temporal Logic (FOLTL) is particularly convenient to specify distributed systems, in particular because of the unbounded aspect of their state space. We have recently exhibited novel decidable fragments of FOLTL which pave the way for tractable verification. However, these fragments are not expressive enough for realistic specifications. In this paper, we propose three transformations to translate a typical FOLTL specification into two of its decidable fragments. All three transformations are proved sound (the associated propositions are proved in Coq) and have a high degree of automation. To put these techniques into practice, we propose a specification language relying on FOLTL, as well as a prototype which performs the verification, relying on existing model checkers. This approach allows us to successfully verify safety and liveness properties for various specifications of distributed systems from the literature.

The arrival of a new operator on the Italian high-speed railway (HSR) market, its maintanance and its market share made Italian open access experience one of the most successful liberalization models in the HSR sector. Researchers noticed that since the entry of the new operator, expansion of Italian HSR market is mostly due to the presence of this new operator. The aim of this article is to establish whether there were some other characteristics of the Italian HSR market that may explain this success even if it may be in opposition with what theory commonly suggests about competition in HSR markets. This research tries to do a complementary analysis by making a comparison with another successful HSR market that is not already liberalized: the French HSR market. After retracing supply, demand and markets maturity of Rome–Milan and Paris–Marseille lines, results reveal that supply and demand evolutions in both markets were very similar, if not identical after the commissioning of HSR. It suggests that liberalization may not be the only explanation of the significant evolution of Italian HSR market but that the opening of new infrastructures may also lead to positive trends that remain until markets reach a high level of maturity. This maturity understood as the residual capacity of the network and partially determined by infrastructure improvement seems to be another variable that had influenced the success of NTV. Indeed, before liberalization, Italian HSR network was far from saturation that allowed new entrant to capture important market shares.

(Conférencier invité); International audience; Chord is a protocol providing a scalable distributed hash table over an underlying peer-to-peer network. It is very popular due to its simplicity, performance and claimed correctness. However, the original version of the Chord maintenance protocol, presented with an informal proof of correctness, was since then shown to be in fact incorrect. It is actually tricky to come up with a provably-correct version as the protocol combines data structures, asynchronous communication, concurrency, and fault tolerance. Additionally, the correctness property amounts to a form of stabilization, a particular kind of liveness property. Previous work only addressed automated proofs of safety; and pen-and-paper, or automated but much bounded, proofs of stabilization. In this article, we report on the first mechanized proof of the liveness property for Chord. Furthermore, our proof addresses the full parameterized version of the protocol, weakens previously-devised invariants and operating assumptions, and is essentially automated (requiring limited effort when manual assistance is needed).

International audience; The Phylog project aims at offering a model-based software-aided certification framework for aeronautical systems based on multi/many-core architectures. Certifying such platforms will entail fulfilling the high level objectives of the MCP-CRI / CAST-32A position paper. Among those, two types of analysis are required: interference and safety analyses. Because of the large size of the platforms and their complexity, those analyses can lead to combinatorial explosion and to some misinterpretation. To tackle these issues, we explore a service-based modelling approach that leads to a simplification of the analyses and to the highlighting of salient properties, making the adaptation of the certification argumentation efficient.

In contrast to the hundreds of scientific papers published on road congestion, very few academic papers have been written on congestion in the rail industry. Most papers focus on scarcity of train paths or, following Petersen (1974), in the relationship between scarcity and speed. However, we could suppose that in rail sector, high traffic density during peak-hours generates an additional delay on others users, so an external cost. In this context, track access charges may reflect the correct marginal social cost of adding a train. The aim of this paper is to use French infrastructure manager data to assess the relationship between traffic and delay. According to the line and its features (allowed speed, number of tracks, signalling…), the econometrical analysis shows a positive econometric relationship between traffic and unreliability rate: an additional train on the line increases the probability of being late for it and for third trains. These results allow computing a marginal cost of congestion, which can be used for pricing and cost benefit analysis of capacity investments. This study may support the implementation of a congestion charge in the French rail network.

International audience; Formal methods and static analysis are widely used in software development, in particular in the context of safety-critical systems. They can be used to prove that the software behaviour complies to its specification: the software correctness. In this article, we address another usage of these methods: the verification of the quality of the source code, i.e., the compliance with guidelines, coding rules, design patterns. Such rules can refer to the structure of the source code through its Abstract Syntax Tree (AST) or to execution paths in the Control Flow Graph (CFG) of functions. AST and CFGs offer complementary information and current methods are not able to exploit both of them simultaneously. In this article, we propose an approach to automatically verifying the compliance of an application with specifications (coding rules) that reason about both the AST of the source code and the CFG of its functions. To formally express the specification, we introduce FO++, a logic defined as a temporal extension of many-sorted first-order logic. In our framework, verifying the compliance of the source code comes to the model-checking problem for FO++. We present a correct and complete model checking algorithm for FO++ and establish that the model checking problem of FO++ is PSPACE-complete. This approach is implemented into Pangolin, a tool for analyzing C++ programs. We use Pangolin to analyze two middle-sized open-source projects, looking for violations of six coding rules and report on several detected violations.

This paper presents the Electrum Analyzer, a free-software tool to validate and perform model checking of Electrum specifications. Electrum is an extension of Alloy that enriches its relational logic with LTL operators, thus simplifying the specification of dynamic systems. The Analyzer supports both automatic bounded model checking, with an encoding into SAT, and unbounded model checking, with an encoding into SMV. Instance, or counter-example, traces are presented back to the user in a unified visualizer. Features to speed up model checking are offered, including a decomposed parallel solving strategy and the extraction of symbolic bounds. Source code: https://github.com/haslab/ElectrumVideo: https://youtu.be/FbjlpvjgMDA., European Regional Development Fund (ERDF) through the Operational Programme for Competitiveness and Internationalisation (COMPETE2020) and by National Funds through the Portuguese funding agency, Fundação para a Ciência e a Tecnologia (FCT) within project POCI-01-0145-FEDER-016826, and the French Research Agency project FORMEDICIS ANR-16-CE25-0007

International audience; This paper describes PHYLOG, a framework in- tended to help certify the use of a multi-core in an aeronautical context. Specific guidelines for such systems have been published in a document, the MCP-CRI / CAST-32A, which provides a series of objectives to be fulfilled. To justify that an objective is indeed achieved, PHYLOG relies on structured graphical no- tations, recursively refining each objective by solving it using a strategy, itself having its own sub-objectives, until all that remains are evidences found either through the use of formal methods, as part of the design choices, or in external documentation. The PHYLOG framework includes such formal methods, providing the means to model the multi-core and to acquire further evidences through automatic analysis.