Assurance for Integrating Advanced Algorithms in Autonomous Safety-Critical Systems

Although advanced algorithms are needed to enable increasingly autonomous civil aviation applications, there are limitations in assurance technologies, which must be addressed to gain trust in the performance of these algorithms. This gap emphasizes the need to guarantee safety by capturing performance boundaries, as these algorithms are integrated. Additionally, multiple similar algorithms might need to be executed sequentially or concurrently to accomplish a mission or provide guidance for safety-critical operations. The selection among algorithm functionalities is a complex and critical activity that needs to be systematically designed and analyzed before actual implementation. Toward this end, we discuss our proposed process, which includes formally modeling abstractions of the algorithms in an architectural framework, then identifying the key performance parameters, followed by verification of the composition of these algorithms with formal contracts based on assumptions and guarantees. Finally, to reduce the gap between design and implementation, an automated translation from the architectural model to source code has been developed, which is a Java-based outline of the implementation. We demonstrate our compositional approach in assuring the behavior of an autonomous aerial system via a collision avoidance case study with advanced algorithms to handle critical emerging situations.