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.

ENTITY

First of all, we introduce the module ENTITY.

#!python
module ENTITY
{
  signature
  {
    [ Entity ]
  }
}

There are two types of entities:

• Interrupt service routines managed by the operating system
• Tasks (basic tasks and extended tasks)

ISR

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 ]
  }
}

TASK

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

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

BASICTASK

#!python
module BASICTASK
{
  imports {
    ex(TASK)
  }
  signature {
    [ BasicTask < Task ]
  }
}

EXTENDEDTASK

#!python
module EXTENDEDTASK
{
  imports {
    ex(TASK)
  }
  signature {
    [ ExtendedTask < Task ]
  }
}

ACTIVITY

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

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

• 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.

INTERRUPTLEVEL

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

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

LOGICALLEVEL

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

TASKLEVEL

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

PROCESSINGLEVEL

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 .
  }
}

ASSIGN

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 following two modules ASSIGN2ISR and ASSIGN2TASK declares static assignment of priorities to interrupt service routines and tasks, respectively.

ASSIGN4ISR

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

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

ASSIGN4TASK

Similarly, an statically assigned priority to a task belongs to taskLevel.

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

ASSIGN4ACTIVITY

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 .
  }
}