Architecture of the OSEK OS

The OSEK operating system serves as a basis for application programs which are independent of each other, and provides their environment on a processor. The OSEK operating system provides a defined set of interfaces for the user. These interfaces are used by entities which are competing for the CPU.

Entities in OSEK OS

First of all, we introduce the module ENTITY.

#!python

module ENTITY
{
  signature
  {
    [ Entity ]
  }
}

A term of the sort Entity represents an entity competing for the CPU.

There are two types of entities: * Interrupt service routines managed by the operating system * Tasks (basic tasks and extended tasks)

A sort of interrupt service routines and a sort of tasks are declared by the following module ISR and TASK, respectively.

#!python

module ISR
{
  imports
  {
    ex(ENTITY)
  }
  signature
  {
    [ ISR < Entity ]
  }
}

The sort ISR is declared as an subsort of Entity. A term of ISR represents an interrupt service routine.

#!python

module TASK
{
  imports {
    ex(ENTITY)
  }
  signature {
    [ Task < Entity ]
  }
}

Similar to ISR, the sort Task is declared as an subsort of Entity. A term of Task denote a task.

The following module is for other activities than interrupt service routines and tasks.

#!python
module ACTIVITY
{
  imports {
    ex(ENTITY)
  }
  signature {
    [ Activity < Entity ]
  }
}

Processing level

OSEK defines three processing levels:

• Interrupt Processing Level
• Logical Level
• Task Level

Within the task level tasks are scheduled (non, full or mixed preemptive scheduling) according to their user assigned priority. The run time context is occupied at the beginning of execution time and is released again once the task is finished.

The following priority rules have been established:

• Interrupts have precedence over tasks
• The interrupt processing level consists of one or more interrupt priority levels
• Interrupt service routines have a statically assigned interrupt priority level
• Assignment of interrupt service routines to interrupt priority levels is dependent on implementation and hardware architecture
• For task priorities and resource ceiling-priorities bigger numbers refer to higher priorities.
• The task's priority is statically assigned by the user

Processing levels are defined for the handling of tasks and interrupt routines. They are regarded as a range of consecutive values. We have already defined the module for intervals on natural numbers. Processing levels can be defined as a constant of the sort Interval/Number.

#!python

module INTERRUPTLEVEL
{
  imports
  {
    ex(INTERVAL/NUMBER)
  }
  signature
  {
    op interruptLevel : -> Interval/Number
  }
  axioms
  {
    eq deducible(nil |- (top(interruptLevel) [>] bot(interruptLevel))) = true .
  }
}

The last equation assures that intervalLevel is not empty, i.e., there is at least one element in intervalLevel.

Logical level and task level can be also defined as constants in the sort Interval/Number.

#!python

module LOGICALLEVEL
{
  imports
  {
    ex(INTERVAL/NUMBER)
  }
  signature
  {
    op logicalLevel : -> Interval/Number
  }
}

#!python

module TASKLEVEL
{
  imports
  {
    ex(INTERVAL/NUMBER)
  }
  signature
  {
    op taskLevel : -> Interval/Number
  }
}

The module PROCESSINGLEVEL defines conditions on priorities of these three processing levels.

#!python

module PROCESSINGLEVEL
{
  imports
  {
    pr(INTERRUPTLEVEL)
    pr(LOGICALLEVEL)
    pr(TASKLEVEL)
  }
  axioms
  {
    vars I J : Number
    eq deducible((I @ interruptLevel),(J @ logicalLevel) |- (I > J)) = true .
    eq deducible((I @ logicalLevel),(J @ taskLevel) |- (I > J)) = true .
    eq deducible((I @ interruptLevel),(J @ taskLevel) |- (I > J)) = true .
  }
}

Assignment of priorities to entities

Priorities are statically assigned to interrupt service routines and tasks before the OSEK OS starts.

#!python

module ASSIGN
{
  imports
  {
    ex(NUMBER)
    ex(ENTITY)
  }
  signature
  {
    op assign : Entity -> Number
  }
}

The operation assign denotes the static assignment of priorities to entities. Let X be an entity, then, assign(X) denotes a priority statically assigned to X.

The following two modules ASSIGN2ISR and ASSIGN2TASK declares static assignment of priorities to interrupt service routines and tasks, respectively.

#!python

module ASSIGN4ISR
{
  imports
  {
    pr(ASSIGN)
    pr(ISR)
    pr(INTERRUPTLEVEL)
  }
  axioms
  {
    vars X : ISR
    eq deducible(nil |- (assign(X) @ interruptLevel)) = true .
  }
}

An statically assigned priority to an interrupt service routine belongs to interrptLevel.

#!python

module ASSIGN4TASK
{
  imports
  {
    pr(ASSIGN)
    pr(TASK)
    pr(TASKLEVEL)
  }
  axioms
  {
    vars X : Task
    eq deducible(nil |- (assign(X) @ taskLevel)) = true .
  }
}

The last module of this section is an assignment of priorities to activities.

#!python
module ASSIGN4ACTIVITY
{
  imports
  {
    pr(ASSIGN)
    pr(ACTIVITY)
    pr(LOGICALLEVEL)
  }
  axioms
  {
    vars X : Activity
    eq deducible(nil |- (assign(X) @ logicalLevel)) = true .
  }
}