The Credo Methodology - Formal Methods for Components and Objects - page 58

E<"{register[0]} & #register[0]==registerSignal";"step"*;
"{openCS[1]} & #openCS[1]==openSignal";
"{request[1],openSS[0]} & #request[1]==key0
& #openSS[0]==openSignal";"#sendRequest[0]==key0";
"{theAnswerIn[0],theAnswerOut[1]}
& #theAnswerIn[0]==#theAnswerOut[1]
& #theAnswerOut[1]==data0";
"{closeSS[0],closeCS[1]} & #closeSS[0]==closeSignal
& #closeCS[1]==closeSignal">
"Manager.request_buffer.state==EMPTY
& Manager.release_buffer.state==EMPTY"
3. We now provide a BTSL formula for the requirement stating that for all
possible executions whenever the dataflow satisfies the dataflow specification
(i.e., it is part of the language defined by the regular expression) then both
buffers will be empty at the end of the execution.
A["{register[0]} & #register[0]==registerSignal";("step"*;
"{openCS[1]} & #openCS[1]==openSignal";
"{request[1],openSS[0]} & #request[1]==key0
& #openSS[0]==openSignal";"#sendRequest[0]==key0";
"{theAnswerIn[0],theAnswerOut[1]}
& #theAnswerIn[0]==#theAnswerOut[1]
& #theAnswerOut[1]==data0";
"{closeSS[0],closeCS[1]} & #closeSS[0]==closeSignal
& #closeCS[1]==closeSignal")+]"
Manager.request_buffer.state==EMPTY
& Manager.release_buffer.state==EMPTY"
4. The next property given in terms of an LTL IO formula asserts that whenever
a server session has been closed in the next step the release buffer of the
network manager will be empty.
G (("#closeSS[0]==closeSignal"
| "#closeSS[1]==closeSignal"
| "#closeSS[2]==closeSignal") ->
X "Manager.release_buffer.state==EMPTY" )
5. The following LTL IO formula represents a fairness condition and ensures that
enabled requests can not be ignored forever. Stated differently, if the request
of a client is enabled at infinitely many positions along a path, then the
request fires at infinitely many locations.
G F "enabled sendRequest[1]" -> G F "sendRequest[1]"
6. The ASL formula given below states that whether there is a strategy that con-
trols, i.e. constraints, the possible dataflow at the three ports ( theAnswerOut[0] ,
theAnswerOut[1] ,and theAnswerOut[2] ), such that for all remaining paths the re-
lease buffer of the network manager stays globally empty.