Wiki
Clone wikiCafeOBJ / OSEK / contents / index-e / backup / 20_Systemservices / 4_Resource_Management
Resource management
Registration
Observation returning a set of resources registered:
#!python module DECLARED-RESOURCE { imports { ex(OBSERVATION2EXTERNALSET) } signature { op declaredResource : -> Observation2ExternalSet } }
Registration of resources:
#!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)) . } }
System services
GetResource:
#!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)))) . } }
ReleaseResource:
#!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)))) . } }
Updated