SafeProver is a formal verification tool that performs both reachability and invariant satisfaction analysis. It uses Bounded Model Checking (BMC) as a refutation technique for counterexample detection and a set of algorithms derived from the K-Induction principle for invariant satisfaction. The proof engine offers the possibility to formally analysis any dicrete-time and bounded system in an exhaustive manner.
Road vehicles - Functional Safety standard ISO 26262 (Part 1, Definition 1.49) defines Freedom From Interference (FFI) as the absence of cascading failures between two or more elements that could lead to the violation of a safety requirement. Element X interferes with Element Y if there exists a failure of Element X that causes Element Y to fail.
A system is Free From Interference, if the failure of any element in the system cannot lead to the failure of any another element. That is, any element is free from interference with respect to all other elements of the system.
Three interference domains are defined in (ISO 26262-6 Annex D): timing and execution, memory management, exchange of information.
This notion can be extended to any piece of software mixing elements of different (safety or security) levels (two or more) without developing all the elements in compliance with the highest level.
Interferences have their origin in
IFFree computes all the Interferences
IFFree Locates the call protections to add to make the application Interference Safe
The ISO 26262: Road vehicles - Functional Safety standard ISO 26262 requires in clause 7.4.14 that "mechanisms for error detection as listed in Table 4 shall be applied". In Table 4 "Detection of data errors" is required for all ASIL levels.
Moreover, clause 7.4.11 states that "it shall be insured that the shared resources are used in such a way that freedom from interference of software partitions is ensured".
A DataRace between two tasks arises when the outcome of the computation of at least one tasks depends on the relative speeds of the tasks. A data race occurs when two instructions access the same memory location and at least one of these accesses is a write.
The Bernstein's equations define conditions for noninterfering computations and avoiding any data race condition. For task Tj, Wj (respectively Rj) denotes the set of global variables written (respectively read or referenced) during the execution of the task.
Two tasks Ti and Tj do not share variables iff: Ri ᴖWj = Ø & Rj ᴖWi = Ø & Wi ᴖWj = Ø.
A variable v is shared between Ti and Tj iff it belongs to one of the subset Ri ᴖWj, Rj ᴖWi or Wi ᴖWj.
Accessing shared variables needs careful control: only one process should access the resource at a time. Mutual exclusion zones are implemented to insure that this property is verified by the code. As a result, a shared variable v raises a data race iff at least one of it accesses is not protected.
The ISO 26262: Road vehicles - Functional Safety standard ISO 26262 (Part 6, Clause 7.4.47) requires "An upper estimation of required resources for the embedded software shall be made, including: the execution time, the storage space (RAM for stack and heaps ...); and the communications resources".
In Table 13 - Methods for software integration testing, method "1d Resource usage test" specifies that "To ensure the fullfilment of requirements influenced by the hardware architectural design with sufficient totlerance, properties such as ... storage usage (RAM for stack and heaps ...) ... have to be determined."
A stack is a last in first out (LIFO) data structure whose primary operations are push and pop. The call stack is divided into tow separate parts: the user stack stores the call procedure’s local data (actual arguments, local variables), the system stack stores the linking information that allow the procedure to return to its caller.
Each thread in a multi-tasking operating system maintains its own stack space.
Independently of the compiler, the user stack follows general rules: the push size is related to the object pushed size, the push address is related to the alignment requirement. To fit the push size and address some padding is added.