Wiki

資源管理

登録

登録されている資源の観測：

#!python

module DECLARED-RESOURCE
{
  imports {
    ex(OBSERVATION2EXTERNALSET)
  }
  signature {
    op declaredResource : -> Observation2ExternalSet
  }
}

資源の登録：

#!python

module DECLARE-RESOURCE
{
  imports {
    ex(REGISTRATION)
    ex(DECLARE)
    ex(INTERFACE)
  }
  signature {
    op DeclareResource : Resource -> Registration
  }
  axioms {
    vars C : System
    vars R : Resource
    eq state(DeclareResource(R)(C)) = declare(R)(state(C)) .
  }
}

システムサービス

資源の占有：

#!python


module GET-RESOURCE
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(OCCUPY)
    pr(DECLARED-RESOURCE)
    pr(ACCESS)
    pr(TASK)
    pr(ISR)
    pr(CURRENT)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op GetResource : External -> SystemService
  }
  axioms {
    vars C : System
    vars R : External
    cq pre(occupy(current(state(C)),R)(state(C)) = true
       if pre(GetResource(R)(C) .
    cq R @ declaredResource(state(C)) = true
       if pre(GetResource(R)(C) .
    cq R @ access(current(state(C))) = true
       if pre(GetResource(R)(C) .
    cq (isISR(current(state(C))) or isTask(current(state(C))))
       if pre(GetResource(R)(C) .
    cq state(GetResource(R)(C)) = occupy(current(state(C)),R)(state(C)) 
       if pre(GetResource(R)(C) .
    cq status(GetResource(R)(C)) = E-OK 
       if pre(GetResource(R)(C) .
    cq status(GetResource(R)(C)) = E-OS-ID
       if not(R @ declaredResource(state(C))) .
    cq status(GetResource(R)(C)) = E-OS-ACCESS
       if not(pre(occupy(current(state(C)),R)(state(C))) or not(R @ access(current(state(C)))) .
  }
}

資源の解放：

#!python

module RELEASE-RESOURCE
{
  imports {
    pr(INTERFACE)
    ex(SYSTEM-SERVICE)
    pr(LEAVE)
    pr(DECLARED-RESOURCE)
    pr(ACCESS)
    pr(TASK)
    pr(ISR)
    pr(CURRENT)
    pr(NORMAL)
    pr(API-ERROR)
  }
  signature {
    op ReleaseResource : External -> SystemService
  }
  axioms {
    vars C : System
    vars R : External
    cq pre(leave(current(state(C)),R)(state(C)) = true
       if pre(ReleaseResource(R)(C) .
    cq R @ declaredResource(state(C)) = true
       if pre(ReleaseResource(R)(C) .
    cq R @ access(current(state(C))) = true
       if pre(ReleaseResource(R)(C) .
    cq (isISR(current(state(C))) or isTask(current(state(C)))) = true
       if pre(ReleaseResource(R)(C) .
    cq state(ReleaseResource(R)(C)) = leave(current(state(C)),R)(state(C)) 
       if pre(ReleaseResource(R)(C) .
    cq status(ReleaseResource(R)(C)) = E-OK 
       if pre(ReleaseResource(R)(C) .
    cq status(ReleaseResource(R)(C)) = E-OS-ID
       if not(R @ declaredResource(state(C))) .
    cq status(ReleaseResource(R)(C)) = E-OS-NOFUNC
       if not(pre(leave(current(state(C)),R)(state(C))) .
    cq status(ReleaseResource(R)(C)) = E-OS-ACCESS
       if not(R @ access(current(state(C)))) .
  }
}