Verification of Group Variables for Detecting Inconsistencies in Software 2015-01-0174

Verification and Validation (V&V) techniques commonly use static analysis to detect property violations in modern software systems. However, besides checking for general programming errors like division by zero, array index out of bound etc., certain program patterns can also be verified in order to detect inconsistencies in the software. For instance, there could be several strongly related program entities, such as groups of variables or data structure members updated together, which are often observed across various parts of a program. We term such strongly related entities as group variables. When only a subset of group variables is updated at some part of a program, it could probably be a result of some inconsistency in implementation which may lead to unexpected behavior or failure of the underlying system. Therefore, verifying group variables and their write operations is essential to ensure the safety and reliability of software.

In this paper, we present a novel application of static analysis to verify write instances of group variables. It includes - a) identification of all potential groups and their corresponding group variables, and b) verification of write operations of identified group variables. We have evaluated the presented technique on four real-world embedded applications for checking its effectiveness, applicability, and scalability. Our technique was successfully able to detect three implementation defects in two well tested real-world applications belonging to automotive industry.