Alarms

The OSEK operating system provides services for processing recurring events. Such events may be for example timers that provide an interrupt at regular intervals, or encoders at axles that generate an interrupt in case of a constant change of a (camshaft or crankshaft) angle, or other regular application specific triggers.

#!python

module ALARM
{
  signature
  {
    [ Alarm ]
  }
}

Counter

The OSEK operating system provides a two-stage concept to process such events. The recurring events (sources) are registered by implementation specific counters. Based on counters, the OSEK operating system software offers alarm mechanisms to the application software.

#!python

module COUNTER
{
  signature
  {
    [ Counter ]
  }
}

A counter is represented by a counter value, measured in ”ticks”, and some counter specific constants. The OSEK operating system does not provide a standardised API to manipulate counters directly. The OSEK operating system takes care of the necessary actions of managing alarms when a counter is advanced and how the counter is advanced.

The OSEK operating system offers at least one counter that is derived from a (hardware or software) timer.

Alarm management

The OSEK operating system provides services to activate tasks, set events or call an alarm-callback routine when an alarm expires. An alarm-callback routine is a short function provided by the application.

#!python

module ALARM-CALLBACK-ROUTINE
{
  imports
  {
    ex(Entity)
  }
  signature
  {
    [ ACR < Entity ]
  }
}

#!python

module EXPIRABLE
{
  import
  {
    pr(OBSERVATION2BOOL)
    pr(ALARM)
  }
  signature
  {
    op expirable : Alarm -> Observation2Bool
  }
}

An alarm will expire when a predefined counter value is reached. This counter value can be defined relative to the actual counter value (relative alarm) or as an absolute value (absolute alarm). For example, alarms may expire upon receipt of a number of timer interrupts, when reaching a specific angular position, or when receiving a message.

#!python

module EXPIRE
{
  imports
  {
    pr(TRANSITION)
    pr(ASSIGNMENT)
    pr(EXPIRABLE)
  }
  signature
  {
    op expire : Alarm -> Transition
    op expired : Alarm -> Transition
  }
  axioms {
    vars C : State
    vars A : Alarm
    cq expirable(A)(C) = true
       if pre(expire(A),C) .
    cq expire(A)(C) = alarm2Transition(A)(expired(A)(C))
       if pre(expire(A),C) .
    eq expirable(A)(expired(A)(C)) = false .
    eq rev(expired(A),expirable(A)) = true .
  }
}

Alarms can be defined to be either single alarms or cyclic alarms. In addition the OS provides services to cancel alarms and to get the current state of an alarm. More than one alarm can be attached to a counter. An alarm is statically assigned at system generation time to:

• one counter
• one task or one alarm-callback routine

Depending on configuration, this alarm-callback routine is called, or this task is activated, or an event is set for this task when the alarm expires. Alarm-callback routines run with category 2 interrupts disabled. Internal task activation and event setting when an alarm expires have the same properties as normal task activation and event setting.

Counters and alarms are defined statically. The assignment of alarms to counters, as well as the action to be performed when an alarm expires, is defined statically, too. Dynamic parameters are the counter value when an alarm shall expire, and the period for cyclic alarms.

#!python
module ALARM-ASSIGNMENT
{
  imports {
    pr(ALARM)
    pr(COUNTER)
    pr(TRANSITION)
  }
  signature {
    op alarm2counter : Alarm -> Counter
    op alarm2Transition : Alarm -> Transition
  }
}