The Importance of Software Architectural Constraints and their Automatic Check
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.
Most importantly, 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. In addition, effectiveness of monitoring safety mechanisms crucially depends on the independence between the monitored element and the monitor.
This is elaborated in quite some details in the automotive functional safety standard ISO 26262, but the same concerns and prescriptions are present, albeit in less precise terms in all other standards: DO-178C, IEC 61508, IEC 62304..., and in the cybersecurity standard ISO/SAE 21434.
What all these standards have in common is that, if software components with different criticalities have to coexist, then there are only two options:
- Develop all software to the same standard as the safety critical software.
- Provide proof that it is not possible for software components with lower criticality to negatively impact components with higher criticality.
Option 1 is often prohibitively expensive, as manufacturers will incur the cost of developing non critical software, such as the in-car entertainment system, to the same safety compliance as critical software such as the braking system. Option 2 is, in almost all cases, a much more cost effective option. Especially because independence/non-interference/segregation at the software level can be checked in a completely automatic way.
Visit us at Embedded World 2023 for more
BUGSENG is attending Embedded World both as an exhibitor (booth 4-348) and as a speaker, within the high-quality conference program the fair features. One of our talks, titled "Formal Verification of Software Architectural Constraints" is precisely on this blog topic.
After a recollection of the basic ideas and methodologies of software decomposition, we will illustrate how independence and similar concepts are treated in the various standards. We will 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.
If you haven't registered for EW23 conferences already, do it now! Early bird discounts expire today (January 31st, 2023).
Look for BUGSENG talks in the program:
On top of that, visiting our booth you will be able to meet our team and attend several demos to learn what can be done with ECLAIR. Shortly, a full program will be available here and on our social platforms, this will include times and registration links.
How ECLAIR can help
ECLAIR comes equipped with a formal verifier that allows for the formal, automatic verification of all sorts of architectural constraints. The required formalization of the constraints does not rely on complex logic formalisms and its implementation in the tool ECLAIR has been certified by TÜV SÜD.
This ECLAIR service provides orders-of-magnitude savings in the verification of independence among software components. All that users have to do is providing the formalization of allowed interactions, and ECLAIR will produce a violation message for each unwanted interaction. ECLAIR will enforce whatever access constraints the user configures, not just safety issues.
All this combines perfectly with the deployment of ECLAIR within a continuous integration infrastructure, such as Jenkins, GitLab or GitHub. The continuous verification of compliance with the architectural constraints, starting from the project early stages, is a dramatically more cost effective option than the alternative, which is to check them, perhaps manually, at a later of the final stage of the project.
Register to next ECLAIR Presentation
A monthly introduction to ECLAIR Software Verification Platform held by BUGSENG experts. This is particularly useful to optimize the evaluation process of the tool or even to get you up to speed on the latest features. This presentation is highly interactive and therefore attendance is limited. A final Q&A session also allows attendees to dig deeper into their requirements and curiosities.
Don't forget to join our LinkedIn community to keep up to date with all our news. Also, subscribe to BUGSENG YouTube channel to strengthen your knowledge of the safe and secure software world. Our videos dive into functional safety, tool qualification, MISRA compliance and so much more.