66 F.Xu et al. (HStmts)s::=schedy(assert b|end 1;2$1+ (HAPISet)::={f11,...,fnsn} (HEvtSet)::so,...,N-1] (HSched)x∈HAbSt--TaskId→Prop (TaskId④t∈Nat (HOSCode)::=(p,E,x) (HProg)P::=(A,O) (HAbsSt∑：={a121,.,an2n} (HDataNm)a ::tcbls ctid... (HData) 2=alt|.… (HStatus)ts::=rdy... (HTCBLs)a ::=t(pri,ts1,...),...,tn(prn;tsn,...)} Fig.3.High-level spec.language and abstract states representation of kernel states is modeled as algebraic abstract states at the high level.This section presents the high-level language and its semantics. As shown in Fig.3,the whole high-level program P consists of the application code A and the abstract specification of the kernel O.The application code A is the same as in the low-level language (see Fig.2).O contains the specifications for kernel APIs,e for interrupt handlers,and x for the scheduler. Programmers at this level have no control over interrupts (e.g.,enabling or disabling interrupts).Always enabled,interrupts are modeled implicitly as abstract external events that may occur non-deterministically at any program points.At the high level an incoming level-k event is always handled by executing e(k),i.e.the k-th handler specified in s. The system APIs and interrupt handlers are specified as an abstract state- ment s,which forms a simple but expressive specification language.sched does scheduling.Its semantics is determined by the abstract scheduler specification X.As defined in Fig.3,x is a binary relation between abstract states and task identifiers.That is,given an abstract state (defined at the bottom of Fig.3),x finds a related task identifier as the next task to execute.Note that x is a relation instead of a function,therefore the abstract scheduler could be non-deterministic. Since x is provided as part of the kernel specification,the semantics of sched in our language is configurable.Specifying details of the scheduling policies(instead of using a more abstract non-deterministic scheduler that may pick any task) allows us to specify and verify scheduling properties such as PIF at the high level. ()is a meta-level relation(defined in Coq)that takes as arguments and maps an abstract state to another.It can be instantiated to specify any atomic transitions over abstract states.assert b asserts that the predicate b holds over the current abstract state.end represents the end of abstract APIs or interrupt handlers.s1;s2 and s1+s2 are statements for sequential composition and non- deterministic choices respectively. Abstract States.The kernel state is represented as the abstract state at the high level.As defined at the bottom of Fig.3,is a mapping from names a to the abstract data Here tcbls is the name for the high-level abstract TCB list a,which maps task identifiers to abstract tasks,including the priority pr66 F. Xu et al. (HStmts) ::= sched | γ(¯v)| assert | end | 1; 2 | 1+ 2 (HAPISet) ϕ ::= {f1 1,...,fn n} (HEvtSet) ε ::= [ 0,..., N−1] (HSched) χ ∈ HAbsSt → TaskId → Prop (TaskId) t ∈ Nat (HOSCode) O ::= (ϕ, ε, χ) (HProg) P ::= (A, O) (HAbsSt) Σ ::= { 1 Ω1,..., n Ωn} (HDataNm) ::= tcbls| ctid | ... (HData) Ω ::= α |t| ... (HStatus) ts ::= rdy | ... (HTCBLs) α ::= {t1 (pr1, ts1,...),. . ., tn (prn, tsn,...)} Fig. 3. High-level spec. language and abstract states representation of kernel states is modeled as algebraic abstract states at the high level. This section presents the high-level language and its semantics. As shown in Fig. 3, the whole high-level program P consists of the application code A and the abstract specification of the kernel O. The application code A is the same as in the low-level language (see Fig. 2). O contains the specifications ϕ for kernel APIs, ε for interrupt handlers, and χ for the scheduler. Programmers at this level have no control over interrupts (e.g., enabling or disabling interrupts). Always enabled, interrupts are modeled implicitly as abstract external events that may occur non-deterministically at any program points. At the high level an incoming level-k event is always handled by executing ε(k), i.e. the k-th handler specified in ε. The system APIs and interrupt handlers are specified as an abstract state￾ment s, which forms a simple but expressive specification language. sched does scheduling. Its semantics is determined by the abstract scheduler specification χ. As defined in Fig. 3, χ is a binary relation between abstract states and task identifiers. That is, given an abstract state Σ (defined at the bottom of Fig. 3), χ finds a related task identifier as the next task to execute. Note that χ is a relation instead of a function, therefore the abstract scheduler could be non-deterministic. Since χ is provided as part of the kernel specification, the semantics of sched in our language is configurable. Specifying details of the scheduling policies (instead of using a more abstract non-deterministic scheduler that may pick any task) allows us to specify and verify scheduling properties such as PIF at the high level. γ(¯v) is a meta-level relation (defined in Coq) that takes ¯v as arguments and maps an abstract state to another. It can be instantiated to specify any atomic transitions over abstract states. assert b asserts that the predicate b holds over the current abstract state. end represents the end of abstract APIs or interrupt handlers. s1; s2 and s1+s2 are statements for sequential composition and non￾deterministic choices respectively. Abstract States. The kernel state is represented as the abstract state Σ at the high level. As defined at the bottom of Fig. 3, Σ is a mapping from names a to the abstract data Ω. Here tcbls is the name for the high-level abstract TCB list α, which maps task identifiers to abstract tasks, including the priority pr