Safety Transformations: Sound and Complete?

摘要

Safety transformations transform unsafe original software into safe software that, in contrast to the unsafe version, detects if its execution was incorrect due to execution errors. Especially transformations based on arithmetic codes such as an AN- or ANB-code apply complex and error-prone transformations, while at the same time aiming for safety- or mission-critical applications. Testing and error injection are used so far to ensure correctness and error detection capabilities. But both are incomplete and might miss errors that change functionality or reduce error detection rates. Our research provides tools for a complete analysis of AN-encoding safety transformations. This paper presents our analysis tools and results for the AN-encoded operations. While we were able to demonstrate functional correctness, we discovered bugs that prevent propagation of errors almost completely for AN-encoded divisions and reduce propagation significantly for logical bitwise operations.