Wiki

割込処理

これまでに紹介していなかった，観測や遷移の記述を紹介した後，割込に関するシステムサービスを記述する．

観測

os-interrupt：

#!python

module OS-INTERRUPT
{
  imports {
    pr(ISR)
  }
  signature {
    op isOSInterrupt : ISR -> Bool
  }
}

isr-state：

#!python

module ISR-AVAILABLE
{
  imports {
    ex(OBSERVATION2BOOL)
  }
  signature {
    op isrAvailable : -> Observation2Bool
  }
}

isr-disabled：

#!python

module ISR-DISABLED
{
  imports {
    ex(OBSERVATION2BOOL)
  }
  signature {
    op isrDisabled : -> Observation2Bool
  }
}

isr-suspended：

#!python

module ISR-SUSPENDED
{
  imports {
    ex(OBSERVATION2BOOL)
  }
  signature {
    op isrSuspended : -> Observation2Bool
  }
}

os-isr-available；

#!python

module OS-ISR-AVAILABLE
{
  imports {
    ex(OBSERVATION2BOOL)
  }
  signature {
    op OSisrAvailable : -> Observation2Bool
  }
}

os-isr-disabled：

#!python

module OS-ISR-DISABLED
{
  imports {
    ex(OBSERVATION2BOOL)
  }
  signature {
    op OSisrDisabled : -> Observation2Bool
  }
}

os-isr-suspended：

#!python

module OS-ISR-SUSPENDED
{
  imports {
    ex(OBSERVATION2BOOL)
  }
  signature {
    op OSisrSuspended : -> Observation2Bool
  }
}

executing

#!python

module EXECUTING
{
  imports {
    ex(OBSERVATION2BOOL)
    pr(CURRENT)
    pr(ISR)
  }
  signature {
    op executing : ISR -> Observation2Bool
  }
  axioms {
    vars C : State
    vars I : ISR
    eq executing(I)(C) = I == current(C) .
  }
}

pending

#!python

module PENDING
{
  imports {
    ex(EXECUTING)
  }
  signature {
    op pending : ISR -> Observation2Bool
  }
  axioms {
    vars C : State
    vars I : ISR
    eq pending(I)(C) = I @ active(C) and not(executing(I)(C)) .
  }
}

遷移

disable-all：

#!python

module DISABLE-ALL
{
  imports {
    ex(TRANSITION)
    pr(ISR-AVAILABLE)
    pr(ISR-DISABLED)
    pr(OS-ISR-AVAILABLE)
    pr(OS-ISR-DISABLED)
  }
  signature {
    op disableAll : -> Action
  }
  axioms {
    vars C : State
    cq isrAvailable(C) = true
       if pre(disableAll,C) .
    cq OSisrAvailable(C) = true
       if pre(disableAll,C) .
    eq isrAvailable,disableAll(C)) = false .
    eq OSisrAvailable,disableAll(C)) = false .
    eq isrDisabled,disableAll(C)) = true .
    eq OSisrDisabled,disableAll(C)) = true .
    eq rev(isrAvailable,disableAll) = true .
    eq rev(OSisrAvailable,disableAll) = true .
    eq rev(isrDisabled,disableAll) = true .
    eq rev(OSisrDisabled,disableAll) = true .
  }
}

enable-all：

#!python

module ENABLE-ALL
{
  imports {
    ex(TRANSITION)
    pr(ISR-AVAILABLE)
    pr(ISR-DISABLED)
    pr(OS-ISR-AVAILABLE)
    pr(OS-ISR-DISABLED)
  }
  signature {
    op enableAll : -> Action
  }
  axioms {
    vars C : State
    cq isrDisabled(C) = true
       if pre(enableAll,C) .
    cq OSisrDisabled(C) = true
       if pre(enableAll,C) .
    eq isrAvailable,enableAll(C)) = true .
    eq OSisrAvailable,enableAll(C)) = true .
    eq isrDisabled,enableAll(C)) = false .
    eq OSisrDisabled,enableAll(C)) = false .
    eq rev(isrAvailable,enableAll) = true .
    eq rev(isrDisabled,enableAll) = true .
    eq rev(OSisrAvailable,enableAll) = true .
    eq rev(OSisrDisabled,enableAll) = true .
  }
}

resume-all

#!python

module RESUME-ALL
{
  imports {
    ex(TRANSITION)
    pr(ISR-AVAILABLE)
    pr(ISR-SUSPENDED)
    pr(OS-ISR-AVAILABLE)
    pr(OS-ISR-SUSPENDED)
  }
  signature {
    op resumeAll : -> Action
  }
  axioms {
    vars C : State
    cq isrSuspended(C) = true
       if pre(resumeAll(C) .
    cq OSisrSuspended(C) = true
       if pre(resumeAll(C) .
    eq isrAvailable,resumeAll(C)) = true .
    eq OSisrAvailable,resumeAll(C)) = true .
    eq isrSuspended,resumeAll(C)) = false .
    eq OSisrSuspended,resumeAll(C)) = false .
    eq rev(isrAvailable,resumeAll) = true .
    eq rev(OSisrAvailable,resumeAll) = true .
    eq rev(isrSuspended,resumeAll) = true .
    eq rev(OSisrSuspended,resumeAll) = true .
  }
}

resume-os

#!python

module RESUME-OS
{
  imports {
    ex(TRANSITION)
    pr(OS-ISR-AVAILABLE)
    pr(OS-ISR-SUSPENDED)
  }
  signature {
    op resumeOS : -> Action
  }
  axioms {
    vars C : State
    cq OSisrSuspended(C) = true
       if pre(resumeOS(C) .
    eq OSisrAvailable,resumeOS(C)) = true .
    eq OSisrSuspended,resumeOS(C)) = false .
    eq rev(OSisrAvailable,resumeOS) = true .
    eq rev(OSisrSuspended,resumeOS) = true .
  }
}

suspend-all

#!python

module SUSPEND-ALL
{
  imports {
    ex(TRANSITION)
    pr(ISR-AVAILABLE)
    pr(ISR-SUSPENDED)
    pr(OS-ISR-AVAILABLE)
    pr(OS-ISR-SUSPENDED)
  }
  signature {
    op suspendAll : -> Action
  }
  axioms {
    vars C : State
    cq isrAvailable(C) = true
       if pre(suspendAll(C) .
    cq OSisrAvailable(C) = true
       if pre(suspendAll(C) .
    eq isrAvailable,suspendAll(C)) = false .
    eq isrSuspended,suspendAll(C)) = true .
    eq OSisrAvailable,suspendAll(C)) = false .
    eq OSisrSuspended,suspendAll(C)) = true .
    eq rev(isrAvailable,suspendAll) = true .
    eq rev(isrSuspended,suspendAll) = true .
    eq rev(OSisrAvailable,suspendAll) = true .
    eq rev(OSisrSuspended,suspendAll) = true .
  }
}

suspend-os

#!python

module SUSPEND-OS
{
  imports {
    pr(COMPLEMENT)
    ex(TRANSITION)
    pr(OS-ISR-AVAILABLE)
    pr(OS-ISR-SUSPENDED)
  }
  signature {
    op suspendOS : -> Action
  }
  axioms {
    vars C : State
    cq OSisrAvailable(C) = true
       if pre(suspendOS(C) .
    eq OSisrAvailable,suspendOS(C)) = false .
    eq OSisrSuspended,suspendOS(C)) = true .
    eq rev(OSisrAvailable,suspendOS) = true .
    eq rev(OSisrSuspended,suspendOS) = true .
  }
}

cause

#!python

module CAUSE
{
  imports {
    ex(ENABLE)
    pr(ISR-AVAILABLE)
    pr(OS-ISR-AVAILABLE)
    pr(OS-INTERRUPT)
  }
  signature {
    op cause : ISR -> Enable
  }
  axioms {
    vars C : State
    vars I : ISR
    cq I @ inactive(C) = true
       if pre(cause(I)(C) .
    cq isOSInterrupt(I) = false
       if pre(cause(I)(C) .
    cq isrAvailable(C) = true
       if pre(cause(I)(C) .
    cq I @ inactive(C) = true
       if pre(cause(I)(C) .
    cq isOSInterrupt(I) = true
       if pre(cause(I)(C) .
    cq OSisrAvailable(C) = true
       if pre(cause(I)(C) .
  }
}

finish

#!python

module FINISH
{
  imports {
    ex(DISABLE)
    pr(ISR)
  }
  signature {
    op finish : ISR -> Disable
  }
  axioms {
    vars C : State
    vars I : ISR
    eq sub(finish(I)) = I .
    cq I @ active(C) = true
       if pre(finish(I),C)) .
  }
}

システムサービス

enable-all-interrupts

#!python

module ENABLE-ALL-INTERRUPTS
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(ENABLE-ALL)
    pr(CURRENT)
    pr(ISR)
    pr(TASK)
  }
  signature {
    op EnableAllInterrupts : -> SystemService
  }
  axioms {
    vars C : System
    cq pre(enableAll(state(C)) = true
       if pre(EnableAllInterrupts(C) .
    cq (isISR(current(state(C))) or isTask(current(state(C)))) = true
       if pre(EnableAllInterrupts(C) .
    cq state(EnableAllInterrupts(C)) = enableAll(state(C)) if pre(EnableAllInterrupts(C) .
  }
}

disable-all-interrupts

#!python

module DISABLE-ALL-INTERRUPTS
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(DISABLE-ALL)
    pr(CURRENT)
    pr(ISR)
    pr(TASK)
  }
  signature {
    op DisableAllInterrupts : -> SystemService
  }
  axioms {
    vars C : System
    cq pre(disableAll(state(C)) = true
       if pre(DisableAllInterrupts(C) .
    cq (isISR(current(state(C))) or isTask(current(state(C)))) = true
       if pre(DisableAllInterrupts(C) .
    cq state(DisableAllInterrupts(C)) = disableAll(state(C)) 
       if pre(DisableAllInterrupts(C) .
  }
}

resume-all-interrupts

#!python

module RESUME-ALL-INTERRUPTS
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(RESUME-ALL)
    pr(CURRENT)
    pr(ISR)
    pr(TASK)
  }
  signature {
    op ResumeAllInterrupts : -> SystemService
  }
  axioms {
    vars C : System
    cq pre(resumeAll(state(C)) = true
       if pre(ResumeAllInterrupts(C) .
    cq (isISR(current(state(C))) or isTask(current(state(C)))) = true
       if pre(ResumeAllInterrupts(C) .
    cq state(ResumeAllInterrupts(C)) = resumeAll(state(C)) 
       if pre(ResumeAllInterrupts(C) .
  }
}

suspend-all-interrupts

#!python

module SUSPEND-ALL-INTERRUPTS
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(SUSPEND-ALL)
    pr(CURRENT)
    pr(ISR)
    pr(TASK)
  }
  signature {
    op SuspendAllInterrupts : -> SystemService
  }
  axioms {
    vars C : System
    cq pre(suspendAll(state(C)) = true
       if pre(SuspendAllInterrupts(C) .
    cq (isISR(current(state(C))) or isTask(current(state(C)))) = true
       if pre(SuspendAllInterrupts(C) .
    cq state(SuspendAllInterrupts(C)) = suspendAll(state(C)) 
       if pre(SuspendAllInterrupts(C) .
  }
}

resume-os-interrupts

#!python

module RESUME-OS-INTERRUPTS
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(RESUME-OS)
    pr(CURRENT)
    pr(ISR)
    pr(TASK)
  }
  signature {
    op ResumeOSInterrupts : -> SystemService
  }
  axioms {
    vars C : System
    cq pre(resumeOS(state(C)) = true
       if pre(ResumeOSInterrupts(C) .
    cq (isISR(current(state(C))) or isTask(current(state(C)))) = true
       if pre(ResumeOSInterrupts(C) .
    cq state(ResumeOSInterrupts(C)) = resumeOS(state(C)) 
       if pre(ResumeOSInterrupts(C) .
  }
}

suspend-os-interrupts

#!python

module SUSPEND-OS-INTERRUPTS
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(SUSPEND-OS)
    pr(CURRENT)
    pr(ISR)
    pr(TASK)
  }
  signature {
    op SuspendOSInterrupts : -> SystemService
  }
  axioms {
    vars C : System
    cq pre(suspendOS(state(C)) = true
       if pre(SuspendOSInterrupts(C) .
    cq (isISR(current(state(C))) or isTask(current(state(C)))) = true
       if pre(SuspendOSInterrupts(C) .
    cq state(SuspendOSInterrupts(C)) = suspendOS(state(C))
       if pre(SuspendOSInterrupts(C) .
  }
}