OSIRIS: Assertion-Based Verification for embedded software

OSIRIS enables the runtime Assertion-Based Verification of (embedded) software, for verifying requirements about the software behaviour.
It can be used to debug the algorithm itself or its implementation, to perform the online monitoring of fault-tolerance or security properties. Its property checkers can also serve as online performance analysis components. For example, it can help verify properties like:

• Everytime variable V1 reaches a given value, function F will be called with 0 as first parameter before a given condition holds for variable V2
• Everytime function G is called with a positive number as second parameter, a given condition on its local variables and some global variables remains true during its execution
• Everytime sensors detect some unexpected values, the reaction of the software is such that a given condition holds for variable V until a nominal situation is restored
• Each new acquired data is fully processed in less than a given amount of time.

Such properties are formalized in PSL (IEEE standard 1850). The software is automatically instrumented with assertion checkers associated with these requirements, such that their satisfaction can be checked during execution/testing.

Methodology

The method is based on event-triggered monitoring of the software.
We consider that observation points are when the assertion needs to be re-evaluated i.e., each time a variable of the assertion has possibly been consulted or modified, or a function of the assertion has been called. In other words, events that will trigger checker’s evaluations are updatings and readings of program variables (both global and local), and function calls or returns (with possible consideration of parameter/return values). Technically, we use a model that allows to observe these events and to trigger the monitors when needed. This model is inspired by the well-known observer pattern.

The first version of the tool proceeded to instrumentation of the source code to enable such an event-driven activation of temporal assertion checkers [CM15].
The current version performs binary instrumentation [BP19]. It automatically instruments object files, thus providing more flexibility than source instrumentation.

Among the case studies (experiments performed on a ARM Cortex-A7):

• A path-following controller: correct reactions of the software to follow the expected path according to values detected by sensors.
• An audio decoding platform: (1) correct reactions of the software to stop the processor clock when the output buffer is full until a DAC interrupt, (2) decoding a frame is never longer than reading it, (3) every frame is fully processed in less than 5 ms.

References

• [BP19] E.Brignon, L.Pierre : "Assertion-Based Verification through Binary Instrumentation". Proc. DATE'2019, Florence (Italy), March 2019.
• [CM15] M.Chabot, K.Mazet, L.Pierre : "Automatic and Configurable Instrumentation of C Programs with Temporal Assertion Checkers". Proc. ACM/IEEE International Conference on Formal Methods and Models for Codesign, Austin (TX), September 2015. See here.

Contact

Prof. Laurence PIERRE
TIMA Laboratory
Laurence.Pierreimag.fr (Laurence[dot]Pierre[at]univ-grenoble-alpes[dot]fr)
Tel. +33 (0)4 76 57 49 92