Wiki
Clone wikiCafeOBJ / OSEK / contents / index-e / backup / 20_Systemservices / 2_Task_Management
Task management
Data types
Task identifier:
#!python module TASK-ID { imports { pr(TASK) pr(NIL) } signature { [ TaskId ] op INVALID-TASK : -> TaskId op id : Task -> TaskId op id : Nil -> TaskId } axioms { eq id(nil) = INVALID-TASK . } }
#!python module TASK-STATE { imports { ex(RESULT) } signature { [ TaskState < Result ] op RUNNING : -> TaskState op SUSPENDED : -> TaskState op READY : -> TaskState op WAITING : -> TaskState } }
Constructional elements
Declare Task:
#!python module DECLARE-TASK { imports { ex(REGISTRATION) ex(DECLARE) } signature { op DeclareTask : Task -> Registration } axioms { vars C : System vars T : Task vars F : Filter eq state(DeclareTask(T)(C)) = declare(T)(state(C)) . } }
Observations
Observation of task identifier:
#!python module OBSERVATION2TASKID { imports { ex(TASK-ID) } signature { [ Observation2TaskId < Observation ] [ TaskId < Value ] op __ : Observation2TaskId Container -> Observation2TaskId } }
#!python module RESULT-TASK-ID { imports { ex(OBSERVATION2TASKID) } signature { op taskId : -> Observation2TaskId } }
#!python module OBSERVATION2TASKSTATE { imports { ex(TASK-STATE) } signature { [ Observation2TaskState < Observation ] [ TaskState < Value ] op __ : Observation2TaskState Container -> Observation2TaskState } }
#!python module RESULT-TASK-STATE { imports { ex(OBSERVATION2TASKSTATE) } signature { op taskState : -> Observation2TaskState } }
System Services
ActivateTask:
#!python module ACTIVATE-TASK { imports { ex(SYSTEM-SERVICE) pr(ACTIVATE) pr(ISR) pr(CURRENT) pr(OCCURRENCE) pr(MULTIPLICITY) pr(SUSPENDED) pr(NORMAL) pr(API-ERROR) } signature { op ActivateTask : Task -> SystemService } axioms { vars C : System vars T : Task cq pre(activate(T)(state(C)) = true if pre(ActivateTask(T)(C) . cq (isISR(current(state(C))) or isTask(current(state(C)))) = true if pre(ActivateTask(T)(C) . cq state(ActivateTask(T)(C)) = activate(T)(state(C)) if pre(ActivateTask(T)(C) . cq status(ActivateTask(T)(C)) = E-OK if pre(ActivateTask(T)(C) . cq status(ActivateTask(T)(C)) = E-OS-LIMIT if occur(enable(state(C)),T) >= multiplicity(T)(C) . cq status(ActivateTask(T)(C)) = E-OS-ID if occurrence(T(state(C)) == 0 . } }
TerminateTask:
#!python module TERMINATE-TASK { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(TERMINATE) pr(ISR) pr(CURRENT) pr(NORMAL) pr(API-ERROR) } signature { op TerminateTask : -> SystemService } axioms { vars C : System vars T : Task eq pre(terminate(current(state(C)))(state(C)) = true if pre(TerminateTask(C) . cq isTask(current(state(C))) if pre(TerminateTask(C) . cq state(TerminateTask(C)) = terminate(current(state(C)))(state(C)) if pre(TerminateTask(C) . cq status(TerminateTask(C)) = E-OK if pre(TerminateTask(C) . cq status(TerminateTask(C)) = E-OS-CALLEVEL if isISR(current(state(C))) . } }
ChainTask:
#!python module CHAIN-TASK { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(EXCHANGE) pr(ISR) pr(CURRENT) pr(OCCURRENCE) pr(MULTIPLICITY) pr(NORMAL) pr(API-ERROR) } signature { op ChainTask : Task -> SystemService } axioms { vars C : System vars T : Task cq pre(exchange(current(state(C)),T)(state(C)) = true if pre(ChainTask(T)(C) . cq pre(activate(T)(state(C)) = true if pre(ChainTask(T)(C) . cq isTask(current(state(C))) = true if pre(ChainTask(T)(C) . cq state(ChainTask(T)(C)) = exchange(current(state(C)),T)(state(C)) if pre(ChainTask(T)(C) . cq status(ChainTask(T)(C)) = E-OK if pre(ChainTask(T)(C) . cq status(ChainTask(T)(C)) = E-OS-LIMIT if occur(enable(state(C),T) >= multiplicity(T) . cq status(ChainTask(T)(C)) = E-OS-ID if occurrence(T(state(C)) == 0 . cq status(ChainTask(T)(C)) = E-OS-CALLEVEL if isISR(current(state(C))) . } }
#!python module SCHEDULE { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(PAUSE) pr(ISR) pr(CURRENT) pr(NORMAL) pr(API-ERROR) } signature { op Schedule : -> SystemService } axioms { vars C : System vars T : Task cq isTask(current(state(C))) = true if pre(Schedule(C)) . cq pre(pause(current(state(C)))(state(C)) = true if pre(Schedule(C)) . cq state(Schedule(C)) = pause(current(state(C)))(state(C)) if pre(Schedule(C)) . cq status(Schedule(C)) = E-OK if pre(Schedule(C) . cq status(Schedule(C)) = E-OS-CALLEVEL if isISR(current(state(C))) . cq status(Schedule(C)) = E-OS-RESOURCE if occupied(current(state(C)))(state(C)) =/= nil . } }
#!python module GET-TASK { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) ex(RESULT-TASK-ID) pr(RUNNING) pr(NORMAL) pr(API-ERROR) } signature { op GetTask : -> SystemService } axioms { vars C : System vars F : Interface vars T : Task eq state(GetTask(C)) = state(C) . cq taskId(result(GetTask(C))) = id(current(state(C))) if isTask(current(state(C))) . cq taskId(result(GetTask,F(C)))) = taskId(result(GetTask(C))) if not(isTask(current(state(F(C))))) . } }
GetTaskState:
#!python module GET-TASK-STATE { imports { pr(INTERFACE) ex(SYSTEM-SERVICE) pr(RESULT-TASK-STATE) pr(RUNNING) pr(SUSPENDED) pr(READY) pr(WAITING) pr(OCCURRENCE) pr(NORMAL) pr(API-ERROR) } signature { op GetTaskState : Task -> SystemService } axioms { vars C : System vars T : Task cq occurrence(T(state(C)) > 0 = true if pre(GetTaskState(T)(C) . eq state(GetTaskState(T)(C)) = state(C) . cq taskState,result(GetTaskState(T)(C))) = RUNNING if running(T(state(C)) . cq taskState,result(GetTaskState(T)(C))) = SUSPENDED if suspended(T)(state(C)) . cq taskState,result(GetTaskState(T)(C))) = READY if not(running(T(state(C))) and ready(T)(state(C)) . cq taskState,result(GetTaskState(T)(C))) = WAITING if waiting(T)(state(C)) . cq status(GetTaskState(T)(C)) = E-OK if pre(GetTaskState(T)(C) . cq status(GetTaskState(T)(C)) = E-OS-ID if occurrence(T(state(C)) == 0 . } }
Updated