  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.
