1. Toshimi Sawada Avatar Toshimi Sawada
  2. Untitled project
  3. CafeOBJ

Wiki

Clone wiki

CafeOBJ / OSEK / contents / systemservice / alarm

View History

アラーム

登録

#!python

module DECLARED-ALARM
{
  imports {
    ex(OBSERVATION2ALARMS)
  }
  signature {
    op declaredAlarm : -> Observation2Alarms
  }
}

観測

ここでは，システムサービスの記述に使われる観測を挙げる．

cycle

#!python

module CYCLE
{
  imports {
    ex(OBSERVATION2NAT)
    pr(ALARM)
  }
  signature {
    op cycle : Alarm -> Observation2Nat
  }
}

deadline

#!python

module DEADLINE
{
  imports {
    ex(OBSERVATION2NAT)
    pr(ALARM)
  }
  signature {
    op deadline : Alarm -> Observation2Nat
  }
}

remainder

#!python

module REMAINDER
{
  imports {
    ex(OBSERVATION2INT)
  }
  signature {
    op remainder : -> Observation2Int
  }
}

now

#!python

module NOW
{
  imports {
    ex(OBSERVATION2NAT)
    pr(ALARM)
  }
  signature {
    op now : Alarm -> Observation2Nat
  }
}

used-alarm

#!python

module USED-ALARM
{
  imports {
    ex(OBSERVATION2ALARMS)
  }
  signature {
    op usedAlarm : -> Observation2Alarms
  }
}

遷移

システムサービスの記述に用いられる遷移は次の通り．

アラームキャンセル

#!python

module CANCEL
{
  imports {
    ex(TRANSITION)
    pr(USED-ALARM)
  }
  signature {
    op cancel : Alarm -> Transition
  }
  axioms {
    vars C : State
    vars A : Alarm
    cq A @ usedAlarm(C) = true
       if pre(cancel(A)(C)) .
    eq usedAlarm(cancel(A)(C)) = usedAlarm(C) \ A .
    eq rev(usedAlarm,cancel(A)) = true .
  }
}

アラーム発火

#!python

module EXPIRE
{
  imports {
    pr(COMPLEMENT)
    ex(TRANSITION)
    pr(ASSIGNMENT)
    pr(NOW)
    pr(DEADLINE)
  }
  signature {
    op expire : Alarm -> Transition
  }
  axioms {
    vars C : State
    vars A : Alarm
    cq expire(A)(C) = alarm2Transition(A)(C)
       if now(A)(C) == deadline(A)(C) .
    cq expire(A)(C) = C
       if now(A)(C) =/= deadline(A)(C) .
  }
}

絶対値設定

#!python

module SET-ABS
{
  imports {
    ex(TRANSITION)
    pr(DECLARED-ALARM)
    pr(USED-ALARM)
    pr(DEADLINE)
    pr(CYCLE)
    pr(ALARM-BASE)
  }
  signature {
    op setAbs : Alarm Nat Nat -> Transition
  }
  axioms {
    vars C : State
    vars A : Alarm
    vars N M : Nat
    cq A @ declaredAlarm(C) = true
       if pre(setAbs(A,N,M)(C)) .
    cq (A @ usedAlarm(C)) = false
       if pre(setAbs(A,N,M)(C)) .
    cq (0 <= N and N <= maxallowedvalue(alarmBase(A))) = true
       if pre(setAbs(A,N,M)(C)) .
    cq (M =/= 0 implies (mincycle(alarmBase(A)) <= M and M <= maxallowedvalue(alarmBase(A)))) = true
       if pre(setAbs(A,N,M)(C)) .
    cq deadline(A)(setAbs(A,N,M)(C)) = N
       if pre(setAbs(A,N,M)(C)) .
    cq cycle(A)(setAbs(A,N,M)(C)) = M
       if pre(setAbs(A,N,M)(C)) .
    cq usedAlarm(setAbs(A,N,M)(C)) = usedAlarm(C), A
       if pre(setAbs(A,N,M)(C)) .
    eq rev(deadline(A),setAbs(A,N,M)) = true .
    eq rev(cycle(A),setAbs(A,N,M)) = true .
    eq rev(usedAlarm,setAbs(A,N,M)) = true .
  }
}

相対値設定

#!python

module SET-REL
{
  imports {
    ex(TRANSITION)
    pr(DECLARED-ALARM)
    pr(USED-ALARM)
    pr(NOW)
    pr(DEADLINE)
    pr(CYCLE)
    pr(ALARM-BASE)
  }
  signature {
    op setRel : Alarm Nat Nat -> Transition
  }
  axioms {
    vars C : State
    vars A : Alarm
    vars N M : Nat
    cq A @ declaredAlarm(C) = true
       if pre(setRel(A,N,M)(C)) .
    cq (A @ usedAlarm(C)) = false
       if pre(setRel(A,N,M)(C)) .
    cq (0 <= N and N <= maxallowedvalue(alarmBase(A))) = true
       if pre(setRel(A,N,M)(C)) .
    cq (M =/= 0 implies (mincycle(alarmBase(A)) <= M and M <= maxallowedvalue(alarmBase(A)))) = true
       if pre(setRel(A,N,M)(C)) .
    cq now(A)(setRel(A,N,M)(C)) = 0
       if pre(setRel(A,N,M)(C)) .
    cq deadline(A)(setRel(A,N,M)(C)) = N
       if pre(setRel(A,N,M)(C)) .
    cq cycle(A)(setRel(A,N,M)(C)) = M
       if pre(setRel(A,N,M)(C)) .
    cq usedAlarm(setRel(A,N,M)(C)) = usedAlarm(C), A
       if pre(setRel(A,N,M)(C)) .
    eq rev(now(A),setRel(A,N,M)) = true .
    eq rev(deadline(A),setRel(A,N,M)) = true .
    eq rev(cycle(A),setRel(A,N,M)) = true .
    eq rev(usedAlarm,setRel(A,N,M)) = true .
  }
}

カウンタ更新 

#!python


module TICK
{
  imports {
    ex(TRANSITION)
    pr(ALARM)
    pr(NAT)
    pr(NOW)
  }
  signature {
    op tick : Alarm Nat -> Transition
  }
  axioms {
    vars C : State
    vars A : Alarm
    vars N : Nat
    eq now(A)(tick(A,N)(C)) = now(A)(C) + N .
    eq rev(now(A),tick(A,N)) = true .
  }
}


#!python

module DECLARE-ALARM
{
  imports {
    ex(REGISTRATION)
    ex(DECLARE)
    ex(INTERFACE)
  }
  signature {
    op DeclareAlarm : Alarm -> Registration
  }
  axioms {
    vars C : System
    vars A : Alarm
    eq state(DeclareAlarm(A)(C)) = declare(A)(state(C)) .
  }
}

システムサービス

アラーム状態の検索： 

#!python


module GET-ALARM-BASE
{
  imports {
    pr(COMPLEMENT)
    pr(INTERFACE)
    pr(ALARM-BASE)
    ex(SYSTEM-SERVICE)
    pr(DECLARED-ALARM)
    ex(RESULT-ALARM-BASE)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op GetAlarmBase : Alarm -> SystemService
  }
  axioms {
    vars C : System
    vars A : Alarm
    cq A @ declaredAlarm(state(C)) = true
       if pre(GetAlarmBase(A)(C)) .
    eq state(GetAlarmBase(A)(C)) = state(C) .
    cq alarmBase,result(GetAlarmBase(A)(C))) = alarmBase(A) 
       if pre(GetAlarmBase(A)(C) .
    cq status(GetAlarmBase(A)(C)) = E-OK 
       if pre(GetAlarmBase(A)(C) .
    cq status(GetAlarmBase(A)(C)) = E-OS-ID
       if not(A @ declaredAlarm(state(C))) .
  }
}

アラーム検索

#!python

module GET-ALARM
{
  imports {
    pr(COMPLEMENT)
    pr(ALARM-BASE)
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(DECLARED-ALARM)
    pr(USED-ALARM)
    pr(REMAINDER)
    pr(DEADLINE)
    pr(NOW)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op GetAlarm : Alarm -> SystemService
  }
  axioms {
    vars C : System
    vars A : Alarm
    cq A @ declaredAlarm(state(C)) = true
       if pre(GetAlarm(A)(C)) .
    cq A @ usedAlarm(state(C)) = true
       if pre(GetAlarm(A)(C)) .
    cq remainder,result(GetAlarm(A)(C))) = deadline(A)(state(C)) - now(A)(state(C)) 
       if pre(GetAlarm(A)(C) .
    eq state(GetAlarm(A)(C)) = state(C) .
    cq status(GetAlarm(A)(C)) = E-OK 
       if pre(GetAlarm(A)(C) .
    cq status(GetAlarm(A)(C)) = E-OS-ID 
       if not(A @ declaredAlarm(state(C))) .
    cq status(GetAlarm(A)(C)) = E-OS-NOFUNC
       if not(A @ usedAlarm(state(C))) and A @ declaredAlarm(state(C)) .
  }
}

相対値でのアラーム設定：

#!python

module SET-REL-ALARM
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(SET-REL)
    pr(NAT)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op SetRelAlarm : Alarm Nat Nat -> SystemService
  }
  axioms {
    vars C : System
    vars A : Alarm
    vars N M : Nat
    cq pre(setRel(A,N,M)(state(C))) = true
       if pre(SetRelAlarm(A,N,M)(C)) .
    cq state(SetRelAlarm(A,N,M)(C)) = setRel(A,N,M)(state(C)) 
       if pre(SetRelAlarm(A,N,M)(C) .
    cq status(SetRelAlarm(A,N,M)(C)) = E-OK 
       if pre(SetRelAlarm(A,N,M)(C) .
    cq status(SetRelAlarm(A,N,M)(C)) = E-OS-ID
       if not(A @ declaredAlarm(state(C))) .
    cq status(SetRelAlarm(A,N,M)(C)) = E-OS-STATE 
       if A @ usedAlarm(state(C)) .
    cq status(SetRelAlarm(A,N,M)(C)) = E-OS-VALUE
       if not(0 <= N and N <= maxallowedvalue(alarmBase(A))) .
    cq status(SetRelAlarm(A,N,M)(C)) = E-OS-VALUE
       if not(M =/= 0 implies (mincycle(alarmBase(A)) <= M and M <= maxallowedvalue(alarmBase(A)))) .
  }
}

絶対値でアラーム設定：

#!python

module SET-ABS-ALARM
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(SET-ABS)
    pr(NAT)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op SetAbsAlarm : Alarm Nat Nat -> SystemService
  }
  axioms {
    vars C : System
    vars A : Alarm
    vars N M : Nat
    cq pre(setAbs(A,N,M)(state(C))) = true
       if pre(SetAbsAlarm(A,N,M)(C)) .
    cq state(SetAbsAlarm(A,N,M)(C)) = setAbs(A,N,M)(state(C)) 
       if pre(SetAbsAlarm(A,N,M)(C) .
    cq status(SetAbsAlarm(A,N,M)(C)) = E-OK 
       if pre(SetAbsAlarm(A,N,M)(C) .
    cq status(SetAbsAlarm(A,N,M)(C)) = E-OS-ID
       if not(A @ declaredAlarm(state(C))) .
    cq status(SetAbsAlarm(A,N,M)(C)) = E-OS-STATE 
       if A @ usedAlarm(state(C)) .
    cq status(SetAbsAlarm(A,N,M)(C)) = E-OS-VALUE
       if not(0 <= N and N <= maxallowedvalue(alarmBase(A))) .
    cq status(SetAbsAlarm(A,N,M)(C)) = E-OS-VALUE
       if not(M =/= 0 implies (mincycle(alarmBase(A)) <= M and M <= maxallowedvalue(alarmBase(A)))) .
  }
}

アラームキャンセル：

#!python

module CANCEL-ALARM
{
  imports {
    pr(COMPLEMENT)
    pr(ALARM-BASE)
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(DECLARED-ALARM)
    pr(CANCEL)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op CancelAlarm : Alarm -> SystemService
  }
  axioms {
    vars C : System
    vars A : Alarm
    cq pre(cancel(A)(state(C)) = true
       if pre(CancelAlarm(A)(C)) .
    cq state(CancelAlarm(A)(C)) = cancel(A)(state(C)) 
       if pre(CancelAlarm(A)(C) .
    cq status(CancelAlarm(A)(C)) = E-OK 
       if pre(CancelAlarm(A)(C) .
    cq status(CancelAlarm(A)(C)) = E-OS-ID
       if not(A @ declaredAlarm(state(C))) .
    cq status(CancelAlarm(A)(C)) = E-OS-NOFUNC
       if not(A @ usedAlarm(state(C))) and A @ declaredAlarm(state(C)) .
  }
}

Updated