Deviation detection to support safe software modification

安全保证是汽车和航空等领域软件系统最重要的需求之一。这些系统在被允许公开运行之前通常要通过一个繁重而正式的认证过程。认证是一个非常昂贵的过程，公司倾向于坚持他们的认证版本的软件，以避免额外的重新认证成本。然而，软件需要随着时间的推移而发展，以提供新的功能并修复潜在的故障。 MicroPilot是一家位于温尼伯的公司，提供一系列无人机（UAV）自动驾驶仪。最近，该公司正在对他们的自动驾驶软件进行认证，他们希望在软件发展时采用最大限度地减少未来重新认证工作的方法。为了帮助MicroPilot在这个方向上，我们提出了一个自动化的方法，提取软件规格之前和之后的每次修改。该方法将报告两个软件版本之间的偏差，作为待调查的潜在安全问题。这提供了一个框架，以确保认证机构在新的修改后，系统的安全性不会在已经认证的子系统上受到损害。

Safety assurance is among the most vital requirements of software systems in domains such as automative and aviation. These systems typically pass a heavy and formal certification process before being allowed to operate in public. Certification is a very expensive process and companies tend to stick with their certified version of software to avoid extra re-certifying cost. However, software needs to evolve over time to provide new features and repair potential faults. MicroPilot is a Winnipeg-based company that offers a family of Unmanned Aerial Vehicle (UAV) autopilots. Recently, the company is moving toward certifying their autopilot software and they would like to apply approaches that minimizes future effort for re-certification, when the software evolves. To help MicroPilot in this direction, we propose an automated approach for extracting software specification before and after each modification. The approach will report deviations between the two versions of the software, as potential safety issues to be investigated. This provides a framework to assure the certification body that the safety of the system has not been compromised on the already certified subsystems, after the new modifications.