Formal Verification of Software Architectural Constraints

In the development of high-integrity software, all interactions between components must satisfy design constraints. Hierarchical levels must not be bypassed: if the design prescribes that software layer A cannot interact directly with layer C without the intermediation of layer B, this is something that must be verified. If components with different criticalities have to coexist on the same ECU, huge savings are possible if we can prove that lower-criticality components cannot interfere with higher-criticality ones. Effectiveness of monitoring safety mechanisms crucially depends on the independence between the monitored element and the monitor. In this paper, after recollecting the basic ideas and methodologies of software decomposition, we introduce the notions of independence and interference in ISO 26262 and other functional safety standards. We then show how architectural constraints at the software level can be formally verified by means of control and data flow static analyses. This technique allows for the formal verification of the design restricting all interactions between user-defined software elements: this includes dynamic, run-time dependencies such as read or write accesses to shared memory, function calls, passing and returning of data, as well as static dependencies due to header file inclusion and macro expansion. The formalization we present does not rely on complex logic formalisms and its implementation in the tool ECLAIR has been certified by TÜV SÜD.