使敏捷开发流程适配 V 型认证程序
软件工程
2019-05-17 v1 形式语言与自动机理论
摘要
我们提出一种面向交通系统中安全与安保关键组件、以高级别认证(CENELEC 50126/50128、DO 178、CC ISO/IEC 15408)为目标的开发流程。该流程在演进灵活性与持续改进方面遵循“敏捷开发”的目标。然而,它通过特定环境(CVCE)强制保障开发产物(从证明、测试到代码)的整体一致性。具体而言,验证流程围绕基于交互式定理证明系统Isabelle/HOL的形式化开发构建,借助一系列精化证明将应用的业务逻辑关联到操作系统模型,并下至代码与具体硬件模型。我们将该流程及其在CVCE中的支持应用于一个案例研究,其包含铁路系统中里程计服务的模型及其在seL4(一个拥有完备Isabelle开发的安全内核)中的对应实现。在Isabelle中实现的新型技术强制特定认证流程下半形式与形式定义的一致性,以提升其成本效益。本文已于ERTS2018发表。
引用
@article{arxiv.1905.06604,
title = {Making Agile Development Processes fit for V-style Certification Procedures},
author = {Sergio Bezzecchi and Paolo Crisafulli and Charlotte Pichot and Burkhart Wolff},
journal= {arXiv preprint arXiv:1905.06604},
year = {2019}
}
备注
11 pages, 6 figures. Appeared in the online conference publication of ERTS 2018, 31.1. - 2.2.2018, Toulouse, France