Deviation detection to support safe software modification

在汽车和航空等领域，安全保证是软件系统最重要的要求之一。这些系统在被允许在公共场所运行之前，通常要经过严格而正式的认证程序。认证是一个非常昂贵的过程，公司倾向于坚持使用他们的认证版本的软件，以避免额外的重新认证成本。然而，软件需要随着时间的推移而发展，以提供新的特性和修复潜在的错误。

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.