Computer Science Sessions

Title: Optimization in a verified compiler

Bugs have been found in mainstream compilers such as gcc and LLVM. For some safety-critical applications (e.g. fly-by-wire aircraft), industrial users may therefore prefer disabling optimizations so that the compiled code easily matches the source code. This results in poor performance. The CompCert compiler (compcert.org) features a formal proof of correctness: executions of the compiled code are shown to match those of the source code by a theorem whose proof was verified by a software proof assistant.

We have added to this compiler a new backend and new optimizations, which also have to be formally proved correct.

Joint work with Sylvain Boulmé, Cyril Six, Léo Gourdin

Title: A Behaviour-based Approach to Quantitative Validation of Cyber-Physical Systems

Abstract: In this talk we describe a behaviour-based approach to quantitative property validation of Cyber-Physical Systems (CPS). The heterogeneity and complexity of industrial CPS make a behaviour-based approach very desirable since It is widely recognized that it is hard or impossible to derive sound mathematical models for such systems. Quantitative validation means providing, instead of a Boolean answer about property satisfaction, quality measures, such as confidence interval, robustness bound, coverage of the set of tested behaviours over the set of all possible behaviours, etc.

We first discuss the problem of encoding and measuring CPS signal spaces with respect to some approximation quality measures. In particular, we consider signal spaces subject to temporal constraints, namely they must satisfy given timing assumptions or properties. For a set of (usually uncountably many) signals representing CPS behaviours of interest, an approximation quality measure reflects how well a finite set of signals sampled from the original set can replace the original set in terms of property validation. We discuss a number of measures for sets of temporal behaviours: uniformity, epsilon-entropy and discrepancy measures. We then describe methods for generating CPS signals with good approximation quality, by combining sampling (as in Monte Carlo and quasi-Monte Carlo methods) and optimisation. The approach is  finally illustrated on CPS benchmarks in particular in automative control.

Title: A Separation of Concerns Approach for the Verified Modelling of Railway Signalling Rules

Auteurs : Yves Ledru, Akram Idani, Rahma Ben Ayed, Abderrahim Ait Wakrime, Philippe Bon

Abstract: This paper proposes a modelling approach for railway signalling rules.

It adopts a separation of concerns approach similar to the one used in information systems security. It first models the effect of operations, and then specifies permissions involving the agent performing the action and the conditions that must be satisfied before performing this action.
These models are expressed in SecureUML diagrams enhanced with B assertions. It then takes advantage of the B4MSecure tool to translate these diagrams into B machines. It finally relies on the ProB tool to verify the model using model-checking and animation. Model-checking assesses the reachability of desired states, and verifies the absence of accidents. The approach proceeds by introducing human errors, checking their consequences, and deploying counter-measures.

Title: Separation of Concerns in Medical Device Safety Assurance

Title: Combining physics-based simulation, medical image registration, and computer vision to localize pulmonary nodules during video-assisted thoracoscopic surgery

Video-assisted thoracoscopic surgery (VATS) is a minimally invasive surgical technique for the diagnosis and treatment of early-stage lung cancer. During VATS, large lung deformation occurs as a result of a change of patient position and a pneumothorax (lung deflation), which hinders the intraoperative localization of pulmonary nodules. We have thus proposed a twofold, multidisciplinary approach to localize and track a lung nodule during surgery.

The first part of the project consists in finding the intra-operative nodule position. Our method relies on physics-based simulation of deformable organs, which has become a powerful tool for surgical planning, guidance, and training. The lung is first modeled as a biphasic, poroelastic medium with allowance for air evacuation, which enables the Finite Element simulation of the lung deformation and deflation. Elastic registration of pre- and intra-operative medical images provides partial boundary conditions and loads for the model. Simulations are then run iteratively to maximize the similarity between the deformed model and actual images. A retrospective study on five clinical cases showed residual errors in the 5 to 10mm range, which corresponds to a compensation of 75% of the localization error, on average.

The second part of the project is augmented-reality, for real-time superimposition of the nodule position on the endoscopic video. Computer vision and monocular SLAM methods will be presented to track the camera pose and lung movement within the thoracic cavity.

Title: Combining Literate Programming and Code Generation to Improve the Reproducibility and Sustainability of Scientific Computing Software

Title: Software composition at scale: 50 shades of scalability

tbd

Title:  The Evolution of the Epsilon Model Management Platform