Unprecedented Assurance

Unparalleled Trustworthiness

Unparalleled Trustworthiness refers to a new level of support for creating secure and reliable embedded systems in less time and at lower cost. Unparalleled Trustworthiness will be enabled through the commercialization of leading-edge research in performance analysis and formal verification of software. Proving the trustworthiness of OKL4 at a never-before-achieved level in embedded system software will streamline the development of trustworthy systems built on top of the platform. For OKL4, Unparalleled Trustworthiness is the result of the following two outcomes:

• Creation of a complete execution timing model for OKL4, providing comprehensive information on the worst-case execution latencies of kernel functions. Availability of comprehensive timing information for OKL4 enables its use in latency and timing-sensitive applications with extremely high confidence in its behavior.
• An implementation of the OKL4 kernel whose design specification and implementation in C code have been formally proven correct using mathematical methods. The resulting proof of correctness provides assurance to the user that neither their development activity nor device performance will be impacted by defects in underlying platform software.

Back To Top