Library ucos_correct

This file contains two final theorems for verifying functional correctness and PIF of ucos-II. The functional correctness is proved with the refinement program logic that ensures the contextual refinement between the low-level kernel implementations and the high-level specification code. PIF is poved as a safety property with the high-level specification code running on the high-level abstract machine.

Require Import include.
Require Import toprule.
Require Import OSTimeDlyProof.
Require Import OSTimeGetProof.
Require Import OSSemCreateProof.
Require Import OSSemDeleteProof.
Require Import OSSemAcceptProof.
Require Import MboxAcceptProof.
Require Import MboxCreateProof.
Require Import MboxDelProof.
Require Import MboxPendProof.
Require Import MboxPostProof.
Require Import OSSemPendProof.
Require Import OSSemPostProof.
Require Import OSQAcceptProof.
Require Import OSQCreateProof.
Require Import OSQDelProof.
Require Import OSQPendProof.
Require Import OSQPostProof.
Require Import OSQGetMsgProof.
Require Import IntExitProof.
Require Import OSEventRemoveProof.
Require Import OSEventSearchProof.
Require Import OSEventTaskRdy.
Require Import OSEventTaskWait.
Require Import OSEventWaitListInitProof.
Require Import OSSchedProof.
Require Import OSTimeTickProof.
Require Import TimeIntProof.
Require Import ToyIntProof.
Require Import OSMutexAcceptProof.
Require Import OSMutexCreateProof.
Require Import OSMutexDelProof.
Require Import OSMutexPendProof.
Require Import OSMutexPostProof.
Require Import ucos_correctaux.
Require Import PIF_def.
Require Import PIF_aux.

Applying the 'TopRule' to verify kernel APIs, internal functions and interrupt handlers.

Lemma ucos_toprule_sat: TopRule low_level_os_code os_spec ucos_init.

Theorem 'ucos_correct' is the final theorem for the functional correctness of ucos/II, which ensures the contextual refinement between the low-level OS kernel code and their high-level specification code. 'low_level_os_code' is the low-level os code, 'os_spec' is the high-level specifications. 'ucos_init' specifies the initial state.

Theorem ucos_correct: OS_Correctness low_level_os_code os_spec ucos_init.

Theorem 'Unbounded_Priority_Inversion_Free_Proof' is used to verify priority-inversion-freedom (PIF) of mutexes in ucos-II.

Theorem Unbounded_Priority_Inversion_Free_Proof:
  forall client_code T cst O T´ cst´ O´,
    InitTasks T client_code cst O ->
    init_st O ->
    good_client_code client_code ->
    no_nest_client client_code O T cst ->
    hpstepstar (client_code , os_spec´) T cst O T´ cst´ O´ ->
    PREEMP O´ ->
    PIF O´.