使敏捷开发过程适合V型认证过程
Making Agile Development Processes fit for V-style Certification Procedures
摘要：
我们提出了一个过程中的安全和安全的关键组件在运输系统的目标是高层次的认证（CENELEC 50126/50128，DO 178，CC ISO/IEC 15408）的发展。该过程在进化灵活性和持续改进方面坚持“敏捷开发”的目标。然而，它通过特定的环境（CVCE）来加强开发工件（从测试到代码的证明）的整体一致性。特别是，验证过程是建立在一个正式的发展的基础上的交互式定理证明系统Isabelle/HOL，通过链接的业务逻辑的应用程序的操作系统模型，到代码和具体的硬件模型感谢一系列的细化证明。我们适用的过程和它的支持CVCE的案例研究，包括一个模型的里程表服务在铁路系统与其相应的实现集成在sel 4（一个安全的内核，其中存在一个全面的Isabelle开发）。在伊莎贝尔实施的新技术，执行特定的认证过程中的半正式和正式的定义的一致性，以提高其成本效益。该论文已在ERTS 2018上发表。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
