正确性
计算机科学
形式验证
功能验证
验证
智能验证
软件验证
运行时验证
形式化方法
形式等价性检查
航空航天
验证和确认
高级验证
软件工程
可执行文件
系统工程
正式规范
计算机仿真模型的验证与验证
迭代和增量开发
软件
软件开发
程序设计语言
软件建设
工程类
运营管理
统计
数学
航空航天工程
作者
Morgan McColl,Callum McColl,Aaron Pereira,Paulo de Souza,Gervase Tuxworth,René Hexel
标识
DOI:10.1109/aero58975.2024.10521386
摘要
Aerospace systems have the most stringent requirements when it comes to safety and reliability. The harsh environment combined with the immense costs of designing and manufacturing space applications places huge concern over ensuring that applications are dependable and function as desired. Formal verification is a tool to guarantee correctness for software executing on aerospace platforms. The advantage of formal verification is the complete absence of error against a design specification. Many applications leverage formal verification to ensure correctness and even integrate it into the certification process (e.g. DO-178C).Formal verification is a highly complex and computationally intense process that requires validating complex structures and an iterative approach to achieve a final, formally verified design. This process is further complicated in aerospace applications as traditional methods often exhibit behavioural differences between a formally verified model and the final software when deployed onto embedded architectures. Thus, formal verification needs to ensure that the verified design is accurate and representative of the executable on the target platform. Another major limitation of formal verification is that current approaches place formal verification towards the end of a project lifecycle. This creates a waterfall design and validation process that often leads to significant rewrites that prevent iterative verification.This research introduces continuous verification, a methodology consistent with current principles and practices in Agile development. This approach allows the early detection and correction of errors during the early stages of a project lifecycle. Designers can now decompose the system as a whole and implement models iteratively. Continuous verification allows the partial verification of models while the programmer iteratively implements them, allowing the early correction of errors and identification of non-verifiable entities that require different forms of validation. Our approach uses executable models that ensure a continuously verifiable design as each new feature gets verified as the application evolves. At any point in time, the working system is also formally verified.We demonstrate the feasibility of this approach through continuous verification using GitHub workflows that continuously integrate and verify designs on target hardware. Verification is performed on the target hardware itself, ensuring a verified, executable model. We have evaluated this approach using flight software that utilises an FPGA and processor that communicate through a shared memory interface. The software components of this design follow trunk-based development with a formally verified main branch. This software is due to launch on a satellite in October 2024.
科研通智能强力驱动
Strongly Powered by AbleSci AI