Making Agile Development Processes fit for V-style Certification Procedures
Authors:
Sergio Bezzecchi,
Paolo Crisafulli,
Charlotte Pichot,
Burkhart Wolff
Abstract:
We present a process for the development of safety and security critical components in transportation systems targeting a high-level certification (CENELEC 50126/50128, DO 178, CC ISO/IEC 15408). The process adheres to the objectives of an "agile development" in terms of evolutionary flexibility and continuous improvement. Yet, it enforces the overall coherence of the development artifacts (rangin…
▽ More
We present a process for the development of safety and security critical components in transportation systems targeting a high-level certification (CENELEC 50126/50128, DO 178, CC ISO/IEC 15408). The process adheres to the objectives of an "agile development" in terms of evolutionary flexibility and continuous improvement. Yet, it enforces the overall coherence of the development artifacts (ranging from proofs over tests to code) by a particular environment (CVCE). In particular, the validation process is built around a formal development based on the interactive theorem proving system Isabelle/HOL, by linking the business logic of the application to the operating system model, down to code and concrete hardware models thanks to a series of refinement proofs. We apply both the process and its support in CVCE to a case-study that comprises a model of an odometric service in a railway-system with its corresponding implementation integrated in seL4 (a secure kernel for which a comprehensive Isabelle development exists). Novel techniques implemented in Isabelle enforce the coherence of semi-formal and formal definitions within specific certification processes in order to improve their cost-effectiveness . This paper has been published at ERTS2018.
△ Less
Submitted 16 May, 2019;
originally announced May 2019.
Microwave Tomographic Imaging of Cerebrovascular Accidents by Using High-Performance Computing
Authors:
P. -H. Tournier,
I. Aliferis,
M. Bonazzoli,
M. de Buhan,
M. Darbas,
V. Dolean,
F. Hecht,
P. Jolivet,
I. El Kanfoud,
C. Migliaccio,
F. Nataf,
C. Pichot,
S. Semenov
Abstract:
The motivation of this work is the detection of cerebrovascular accidents by microwave tomographic imaging. This requires the solution of an inverse problem relying on a minimization algorithm (for example, gradient-based), where successive iterations consist in repeated solutions of a direct problem. The reconstruction algorithm is extremely computationally intensive and makes use of efficient pa…
▽ More
The motivation of this work is the detection of cerebrovascular accidents by microwave tomographic imaging. This requires the solution of an inverse problem relying on a minimization algorithm (for example, gradient-based), where successive iterations consist in repeated solutions of a direct problem. The reconstruction algorithm is extremely computationally intensive and makes use of efficient parallel algorithms and high-performance computing. The feasibility of this type of imaging is conditioned on one hand by an accurate reconstruction of the material properties of the propagation medium and on the other hand by a considerable reduction in simulation time. Fulfilling these two requirements will enable a very rapid and accurate diagnosis. From the mathematical and numerical point of view, this means solving Maxwell's equations in time-harmonic regime by appropriate domain decomposition methods, which are naturally adapted to parallel architectures.
△ Less
Submitted 19 March, 2020; v1 submitted 9 July, 2016;
originally announced July 2016.
