Talk "Verification of software artifacts in the nuclear domain (an experience report)"

by Carlos Gustavo Lopez Pombo

Mon, 05 February 2024 at 02:00 pm in Salzburg, Austria

Joint work with: Germán Regis & INVAP S.E.

Abstract: Software systems are ubiquitous and, while absence of errors is know to be a highly undecidable problem, there are domains where the expected behavior of the system must come with some form of certification. Paradigmatic examples of such domains are the nuclear field, aerospace, unmanned vehicles and health and, still, all of them have registered tragic events due to software “mishaps”. Most of the software involved in the development of critical systems runs embedded in microcontrollers under very tight constraints regarding the use of resources (i.e., computation time, memory usage, specific hardware devices’ specifications, etc.). These specificities have a huge impact in the guidelines ruling the development process, sometime yielding software artifacts that can be thought of as an integral part of the hardware design. This is specially the case in fields where the development of the required software artifacts is done by the same electronic engineering teams designing the hardware over which they run, like in the case of the nuclear domain. Even in critical domains, like the ones we mentioned before, current quality assurance processes for software artifacts mostly rely only on testing techniques without any formal support and, as a counterpart argument, formal methods are usually presented as tools tailored to analyze application-level characteristics of the software artifacts. In a recent collaboration with INVAP S.E., a leading company in the construction of experimental nuclear reactors, we put forward a set of tools aiming at aiding teams of engineers in the process of design, implement and analyze embedded systems. The toolset consists of a formal, yet reasonably simple, language whose analysis is supported by an automatic tool for runtime verification.