Wiki

Description of system services

Definition of system objects

Within the OSEK operating system all system objects have to be determined statically by the user. The operating system supplier provides the definition of the operating system objects. The actual creation of the objects (unique names and specific characteristics) is done during the system generation phase. The declarations done in the application source are external references to those operating system objects. There are no system services available to dynamically create system objects. Declarations provide information that a system object is to be used which has been created at another location. The names are used as identifiers within the system services.

#!python

module SYSTEM-SERVICE
{
  imports
  {
    ex(INTERFACE)
    pr(CURRENT)
  }
  signature
  {
    [ SystemService < Interface ]
    op available : Entity SystemService System -> Bool
  }
  axioms
  {
    vars F : SystemService
    vars S : System
    vars X : Entity
    cq available(X,F,S) = true
       if pre(F,S) and (X @ current(state(S))) .
  }
}

Conventions

System services are called from tasks, interrupt service routines, hook routines, and alarm- callbacks. Depending on the system service, there may be restrictions regarding the availability. Further restrictions are imposed by the conformance classes.

#!python

    vars T : Task
    vars I1 : ISR1
    vars I2 : ISR2
    vars EH : ErrorHook
    vars PrH : PreTaskHook
    vars PoH : PostTaskHook
    vars SUH : StartupHook
    vars SDH : ShutdownHook
    vars ACR : AlarmCallback
    vars S : System

    eq available(T,ActivateTask,S) = true .
    eq available(I2,ActivateTask,S) = true .

    eq available(T,TerminateTask,S) = true .

    eq available(T,ChainTask,S) = true .

    eq available(T,Schedule,S) = true .

    eq available(T,GetTaskID,S) = true .
    eq available(I2,GetTaskID,S) = true .
    eq available(EH,GetTaskID,S) = true .
    eq available(PrH,GetTaskID,S) = true .
    eq available(PoH,GetTaskID,S) = true .

    eq available(T,GetTaskState,S) = true .
    eq available(I2,GetTaskState,S) = true .
    eq available(EH,GetTaskState,S) = true .
    eq available(PrH,GetTaskState,S) = true .
    eq available(PoH,GetTaskState,S) = true .

    eq available(T,DisableAllInterrupts,S) = true .
    eq available(I1,DisableAllInterrupts,S) = true .
    eq available(I2,DisableAllInterrupts,S) = true .

    eq available(T,EnableAllInterrupts,S) = true .
    eq available(I1,EnableAllInterrupts,S) = true .
    eq available(I2,EnableAllInterrupts,S) = true .

    eq available(T,SuspendAllInterrupts,S) = true .
    eq available(I1,SuspendAllInterrupts,S) = true .
    eq available(I2,SuspendAllInterrupts,S) = true .
    eq available(EH,SuspendAllInterrupts,S) = true .
    eq available(PrH,SuspendAllInterrupts,S) = true .
    eq available(PoH,SuspendAllInterrupts,S) = true .
    eq available(ACR,SuspendAllInterrupts,S) = true .

    eq available(T,ResumeAllInterrupts,S) = true .
    eq available(I1,ResumeAllInterrupts,S) = true .
    eq available(I2,ResumeAllInterrupts,S) = true .
    eq available(EH,ResumeAllInterrupts,S) = true .
    eq available(PrH,ResumeAllInterrupts,S) = true .
    eq available(PoH,ResumeAllInterrupts,S) = true .
    eq available(ACR,ResumeAllInterrupts,S) = true .

    eq available(T,SuspendOSInterrupts,S) = true .
    eq available(I1,SuspendOSInterrupts,S) = true .
    eq available(I2,SuspendOSInterrupts,S) = true .

    eq available(T,ResumeOSInterrupts,S) = true .
    eq available(I1,ResumeOSInterrupts,S) = true .
    eq available(I2,ResumeOSInterrupts,S) = true .

    eq available(T,GetResource,S) = true .
    eq available(I2,GetResource,S) = true .

    eq available(T,ReleaseResource,S) = true .
    eq available(I2,ReleaseResource,S) = true .

    eq available(T,SetEvent,S) = true .
    eq available(I2,SetEvent,S) = true .

    eq available(T,ClearEvent,S) = true .

    eq available(T,GetEvent,S) = true .
    eq available(I2,GetEvent,S) = true .
    eq available(EH,GetEvent,S) = true .
    eq available(PrH,GetEvent,S) = true .
    eq available(PoH,GetEvent,S) = true .

    eq available(T,WaitEvent,S) = true .

    eq available(T,GetAlarmBase,S) = true .
    eq available(I2,GetAlarmBase,S) = true .
    eq available(EH,GetAlarmBase,S) = true .
    eq available(PrH,GetAlarmBase,S) = true .
    eq available(PoH,GetAlarmBase,S) = true .

    eq available(T,GetAlarm,S) = true .
    eq available(I2,GetAlarm,S) = true .
    eq available(EH,GetAlarm,S) = true .
    eq available(PrH,GetAlarm,S) = true .
    eq available(PoH,GetAlarm,S) = true .

    eq available(T,SetRelAlarm,S) = true .
    eq available(I2,SetRelAlarm,S) = true .

    eq available(T,SetAbsAlarm,S) = true .
    eq available(I2,SetAbsAlarm,S) = true .

    eq available(T,CancelAlarm,S) = true .
    eq available(I2,CancelAlarm,S) = true .

    eq available(T,GetActiveApplicationMode,S) = true .
    eq available(I2,GetActiveApplicationMode,S) = true .
    eq available(EH,GetActiveApplicationMode,S) = true .
    eq available(PrH,GetActiveApplicationMode,S) = true .
    eq available(PoH,GetActiveApplicationMode,S) = true .
    eq available(SUH,GetActiveApplicationMode,S) = true .
    eq available(SDH,GetActiveApplicationMode,S) = true .

    eq available(T,ShutdownOS,S) = true .
    eq available(I2,ShutdownOS,S) = true .
    eq available(EH,ShutdownOS,S) = true .
    eq available(SUH,ShutdownOS,S) = true .