Wiki

Conformance classes

The OSEK/VDX specification prepares four conformance classes.

（OSEK/VDX Operating System Specification 2.3.3）

The table indicatiod below describes conditions for automotive operating systems to conform.

（OSEK/VDX Operating System Specification 2.3.3）

We introduce formal descriptions of above conditions in CafeOBJ.

Multiple requesting of task activation

The multiplicity of tasks are declared like:

#!python

module MULTIPLICITY
{
  imports {
    ex(NAT)
    pr(BASICTASK)
    pr(EXTENDEDTASK)
  }
  signature {
    op multiplicity : Task -> Nat
  }
  axioms {
    vars T : BasicTask
    vars X : ExtendedTask
    eq multiplicity(T) > 0 = true .
    eq multiplicity(X) = 1 .
  }
}

The requirement for multiple task activation can be declared as follows:

#!python

module REQUIREMENT-on-MULTIPLICITY
{
  imports
  {
    pr(MULTIPLICITY)
  }
  axioms
  {
    vars T : BasicTask
    eq multiplicity(T) > 1 = true .
  }
{

If multiple request of basic tasks is not permitted, multiplicity of basic tasks is equal to 1.

#!python

module REQUIREMENT-on-MULTIPLICITY
{
  imports
  {
    pr(MULTIPLICITY)
  }
  axioms
  {
    vars C : State
    eq multiplicity(C) = 1 .
  }
{

Number of tasks which are not in the suspended state

The number of tasks which are not in the suspended state is equal to the sum of:

the number of task of ready state
the number of task of running state
the number of task of waiting state.

#!python

module LIMIT
{
  imports
  {
    pr(NAT)
  }
  signature
  {
    op limit : -> Nat
  }
}

#!python

module REQUIREMENTS-on-the-Number-of-nonsuspended-Tasks
(
  X :: LIMIT
{
  imports
  {
    pr(RUNNING)
    pr(READY)
    pr(WAITING)
  }
  axioms
  {
    vars C : State
    eq (#(running(C)) + #(ready(C)) + #(waiting(C))) <= limit = true .
  }
}

This can be included in the pre condition of task activation.

#!python

module REQUIREMENTS-on-the-Number-of-nonsuspended-Tasks
(
  X :: LIMIT
{
  imports
  {
    pr(ENABLE)
    pr(RUNNING)
    pr(READY)
    pr(WAITING)
  }
  axioms
  {
    vars C : State
    vars T : Enable
    cq (#(running(C)) + #(ready(C)) + #(waiting(C))) < limit = true
       if pre(T,C) and isTask(subj(T)) .
  }
}

The condition on limit can be described as follows:

#!python

module LIMIT
{
  imports
  {
    pr(NAT)
  }
  signature
  {
    op limit : -> Nat
  }
  axioms
  {
    eq limit >= 8 = true . -- for BCC1 and BCC2
    eq limit >= 16 = true . -- for ECC1 and ECC2
  }
}

More than one task per priority

This condition is equivalent to the injectivity of the priority assignment operation assign.

#!python

module INJECTIVITY-on-Priority-Assignment-for-Task
{
  imports
  {
    pr(ASSIGN)
  }
  axioms
  {
    vars X Y : Task
    cq (assign(X) = assign(Y)) = false
       if not(X = Y) .
  }
}

The above conditional equation can be described as follows:

#!python

    cq (X = Y) = true
       if assigned(X) = assigned(Y) .

If assign need not to be injective, this condition also do not need to be described.

Number of events per task

This condition can be regarded as a condition on the number of events which one task can own.

#!python

    op count : Events Extended -> Nat
    vars E : Event
    vars S : Events
    vars T : Extended
    eq count(nil,T) = 0 .
    cq count((E,S),T) = 1 + count(S,T) if owner(E) = T .
    cq count((E,S),T) = count(S,T) if not(owner(E) = T) .

This condition can be described as follows:

#!python

module REQUIREMENT-on-EVENTS
{
  imports
  {
    pr(RAISED)
  }
  signature
  {
    op count : Events Extended -> Nat
    op limit : -> Nat
  }
  axioms
  {
    vars C : State
    vars T : Extended
    vars E : Event
    vars S : Events
    eq (count(raised(C),T) <= limit) = true.
    eq (limit >= 8) = true .
    eq count(nil,T) = 0 .
    cq count((E,S),T) = 1 + count(S,T) if owner(E) = T .
    cq count((E,S),T) = count(S,T) if not(owner(E) = T) .
  }
}

Nubmer of task priorities

This condition can be described as a condition on the cardinarity of processing levels.

#!python

module REQUIREMENT-on-TASKLEVEL
{
  imports
  {
    pr(PROCESSING-LEVEL)
  }
  axioms
  {
    eq #(taskLevel) >= 7 -- for BCC1 and BCC2
    eq #(taskLevel) >= 15 -- for ECC1 and ECC2
  }
}

The number of resources

This condition is on the number of registered resources.

#!python

module REQUREMENT-on-RESOURCES
{
  imports
  {
    pr(DECLARED-RESOURCE)
  }
  axioms
  {
    vars C : State
    cq (#declaredResource(C)) >= 8 = true
       if started(C) .
  }
}

where started(C) returns true when the OS has already started.

The number of internal resources

#!python

module REQUIREMENT-on-INTERNAL-RESOUCE
{
  imports
  {
    ex(DECLARED-RESOURCES)
  }
  signature
  {
    op num-of-int : Resources -> Nat
  }
  axioms
  {
    vars C : State
    vars S : Resources
    vars R : Resorce
    cq (num-of-int(C) >= 2) = true
       if started(C)
    eq num-of-int(nil) = 0 .
    cq num-of-int(R,S) = 1 + num-of-int(S)
       if internal(R) .
    cq num-of-int(R,S) = num-of-int(S)
       if external(R) .
  }
}

where internal(R) returns true when R is an internal resource, and external(R) returns true when R is not an internal resource.

The number of alarms

This condition holds if the set of registered alarms is not empty.

#!python

module REQUIREMENT-on-ALARM
{
  import
  {
    pr(DECLARED-ALARM)
  }
  axioms
  {
    vars C : State
    cq (declaredAlarm(C) = nil) = false
       if started(C) .
  }
}

The number of application mode

This condition does not need to be described because the OSEK OS has a default application mode.

Construction of the OSEK OS

The formal description of the OSEK OS can be obtained by the sum of observations, transitions, system services and conditions of a conformance class which the OS conforms to.