Child nodes:
The requirements for the Collision Avoidance decision making have been manually translated from structured English to Gwendolen (application source code) and verified.
A coding standard which constrains the use of the Gwendolen language to a safe subset has been used and the code has been reviewed against this.
The same structured English requirements have been manually translated into Agent Java PathFinder (AJPF) code (the verification model) which is an extension of the NASA Java Pathfinder (JPF) and verified.
A coding standard which constrains the use of the AJPF language to a safe subset has been used and the code has been reviewed against this.
The JPF configuration files are created from a coding standard and reviewed.
The application source code is compiled into Java Byte Code (created from the Gwendolen Model Checking Agent Programming Languages (MCAPL) Framework).
This is then executed within JPF on the Java Virtual Machine on the robot's target processor.
The safety critical hard realtime Java Virtual Machine (JVM) (york.ac.uk have done some work on this!) has been qualified to SIL 3 when used with the Windriver VxWorks Cert Edition Operating System (RTOS) on the <hardware name> platform (or possibly such a JVM could be developed that would execute bare metal).
The JPF and compiled Gwendolyn execute on the RTOS on the robot's target processor.
Any errors and warnings flagged by the execution are documented, analysed and sentenced. An impact analysis determined where bug fixes are required (the bug fixes are not limited to code, they include documentation). Corrective action has been instigated and closed out which includes a review of processes, procedures and coding standards.
When all errors and warnings have been implemented and fully re-verified, the application target code progresses to the non-functional verification.
The non-functional testing is performed in situ on the robot hardware using stimulators as necessary and shown to meet all of the requirements.
The stimulators have been verified.
Verification specifications have been written for all stages of this process which are traceable to requirements specifications.
Verification reports have been written which are traceable to the verification specifications.
Verification specifications and reports are reviewed for correctness and completeness.
The formal verification provides a formal mathematical proof end-to-end (requirements to target code) of the correctness. It also identifies other potential failures such as deadlock.
The complete process and justification for its adequacy is provided in the Design Justification Report.