Part V Requirements
Definition 75: Shared Behaviour
provided by humans or some “gadgets” of the domain,“outside” of our concern.
s819
pfm-shrd-bhvs
Example 97 –Shared Behaviours: Personal Financial Transactions:
67. There is an index set,CI, of clients.
68. For each client there is an “own”
69. ‘personal finance management’ stateπφσci:ΠΦΣ (cf. 50 on page 159).
70. The finance industry “grand state”ω:Ωis as before (cf. Item and formula line 51 on page 159).
71. The system consists of
a) an indexed set ofclient behaviours
b) and one finance industry “grand state” behaviouromega.
72. We model communications between clients and the financial industry to occur over client-industry channels.
73. We model communications over these channels as being of typeM.Mwill be “revealed” as we go
on. s820
type 67 CI
68 ΠΦΣs=CI →m ΠΦΣ
69 ΠΦΣ
70 Ω=Banks×SecTrad×...
value
67 cis:CI-set 68 πφσs:ΠΦΣs 70 ω:Ω
71 system:Unit→Unit 71 system()≡
71a k {client(ci)(πφσs(ci))|ci:CI•ci∈cis} 71b komega(ω)
channel
72 {c ω ch[ci]|ci:CI•ci∈cis} M type
73 M
s821
Let us first consider the issue of events. First the events arise in “the market”, here symbolised with the global stateω:Ω.
74. The omega(ω) behaviour and the client(ci)(πφσs(ci)) behaviours, for all clients, are cyclic — expressed through ‘tail recursion’ over possibly updated states.
75. To model events we let theomega(ω)behaviour alternate between either
a) inquiring its state as to unusual situations in, the statusstatus of, “the market”, and, b) if so, inform an arbitrary subsets ofclients of such “events” and
c) continuing in an unchanged global financial system state or
76. servicingclientrequests — from any client.
s822
type Event value
omega:Ω→in,out{c ω ch[ci]|ci:CI•ci∈cis} Unit omega(ω)≡
75b (let scis:CI-set •scis⊆cisin
75a let event=ωstatus(ωsnapshot(ω))in
75b if nok status(event)then{c ω ch[ci]!event|ci:CI•ci ∈scis} end;
75c omega(ω)end end) 75 ⌈⌉
76 ⌈⌉⌊⌋ {let req=c ω ch[ci]? in...see Items81–88b...end |ci:CI•ci ∈cis} 75a ωsnapshot:Ω→Ω
75a ωstatus:Ω→Event 75b nok status: Event→Bool
s823 Then we consider how clients respondto becoming aware of unusual events in “the market”.
s824
77. Clients alternate between handling events:
78. first deciding (76–78) to “listen to the market”,
a) then updating an own personal finance state (πφσ),
b) and then coming a client behaviour in that new personal finance state, and
79. handling ordinary, that is, personal finance management (pfm) or 80. just idling.
s825
value
77 client: ci:CI→ΠΦΣ →in,outc ω ch[ci] Unit 77 client(ci)(πφσ)≡
78 (letevent=c ω ch[ci]?in
78a let πφσ′ =update πφσ(πφσ)(event) in 78b client(ci)(πφσ′)end end)
77 ⌈⌉
79 client(ci)(pfm session(ci)(πφσ))
77 ⌈⌉
80 client(ci)(πφσ)
s826
Let us now turn to the treatment of usual financial transactions. The main functions, in Example 96, are pfm session(Items 52–60 and formulas on Pages 159–160) andInt Cmd (Items 63–66 and formulas on Pages 160–160) We now analyse these two functions. We refer, in the following to the formula lines on Pages 159–160 and Pages 160–160. The analysis is with respect to what actions,π, are expected to occur in theclientbehaviour and what actions are expected from the financial industry (i.e., to occur in theomegabehaviour).
s827
Inpfm session(Pages 159–160), formula lines
• 53π:obs Responses(πφσ),
• 55π:cli anal mkt(response)(πφσ), • 56π:ifok or nok = ok and
• 59π:merge pfm(response,date,time)(πφσ) are expected from theclientbehaviour, all others from the industry, i.e., theomegabehaviour.
InInt Cmd (Pages 160–160), formula lines
8.8 Interface Requirements 163
are expected from theclientbehaviour. s828
Of the functions itemised above, the
functions — as invoked by the client, in the pfm session and the Int Cmd behaviours — require access to the global financial service industry stateω.
The idea is now, for the client, in its Int Cmd (see Formula lines 61.0 onwards [Page 164]) to communicate these functions, as function named argument lists, cf. Formula lines 81–86 below.
s829
type
FCT==Anal mkt|Obs mkt|...|Open aact|...|Buy Ofr|...
81 Anal mkt=mkAnalMkt(argl:Arg∗) 82 Obs mkt=mkObsMkt(argl:Arg∗) 83 Open acct=mkOpenAcct(argl:Arg∗) 84 ...
85 Buy Ofr=mkBuyOfr(argl:Arg∗) 86 ...
channel
72 {c ω ch[ci]|ci:CI•ci∈cis}: Event|FCT|Response
s830
87. Theomegabehaviour thus alternates
a) between accepting and responding to either of the many forms of functions,FCT b) or generating event notifications.
88. If theomegabehaviour of its own will, that is, internally non-deterministically chooses to accept a client initiate request it externally non-deterministically chooses which client request to serve.
a) Theomegabehaviour deciphers the request;
b) applies the communicated function to (possibly communicated arguments) and the ω”grand state”; and communicates the result back to the chosen client.
s831
value
omega:Ω→in,out{c ω ch[ci]|ci:CI•ci∈cis} Unit omega(ω)≡
87b (let scis:CI-set •scis⊆cisin
87b letevent=ωstatus(ωsnapshot(ω))in
87a ...
87a mkBuyOfr(argl)→
88a let(ω′,res) =int buyofr(argl)(ω)inc ω ch[ci]! res ; omega(ω′)end,
87a ...
88a end end|ci:CI•ci ∈cis} Some auxiliary functions:
s832
value
64π eval obs mkt: Arg∗ →Ω→Response 64π ω anal mkt: Arg∗ →Ω→Response 65 int open acct: Arg∗→Ω →Ω×Response 66 int buyofr: Arg∗ →Ω→Ω×Response
There is only minor changes, marked√, to pfm session: (52) an additional argument, ci:CI and (58) an additional argument, (ci) to Int Cmd(ci)(cmd,argl).
s833
value
52√ pfm session: ci:CI→ΠΦΣ →in,outωch ΠΦΣ 52√ pfm session(ci)(πφσ)≡
53 letpast responses=obs Responses(πφσ)in
54 letresponse=ωch[ci]!mkObsMkt(past responses);ωch[ci]?in 55 letresponse=analyse pfm(past responses)(πφσ)in
56 if advice pfm action(response)
57 then(let (cmd,argl)=what pfm to do(response)in 58√ let response=Int Cmd(ci)(cmd,argl)in
59√ pfm session(ci)(merge pfm(response)(πφσ))end end)end 60 elseπφσ end end end
56 advice pfm action: Response→Bool
55 analyse pfm: Responses→({|ok|}|Event)→ {|ok|nok|}
Similarly the changes to Int Cmd are obvious and marked, as before, with.i, i= 0,1,2,3:
s834
value
61.0 Int Cmd: ci:CI×(Cmd×Arg∗)→in,outωch Response 61 Int Cmd(ci)(cmd,argl)≡
61 casecmdof
61.2 obsmkt→ωch[ci]!mkObsMkt(argl) ;ωch[ci]?
61.2 analpfm→ωch[ci]!mkAnalMkt(argl) ;ωch[ci]?
61 ...
61.2 openacct→ωch[ci]!mkOpenAcct(argl) ;ωch[ci]?
61 ...
61.3 buyofr→ωch[ci]!mkBuyOfr(argl) ;ωch[ci]?
61 ...
61 end
This ends Example 97
Discussion s835
acm-rtre-c
to be written
8.9 Machine Requirements 165
8.9 Machine Requirements
s836acm-rtre-d
Definition 76 – Machine Requirements: By machine requirements we understand those re-quirements that can be expressed sˆolely in terms of (or with prime reference to) machine concepts
8.9.1 An Enumeration of Machine Requirements Issues s837 There are many separable machine requirements. To find one’s way around all these separable machine requirements we shall start by enumerating the very many that we shall overview.
s838
1. Performance Requirements from Page 166
a) Storage Requirements from Page 167
b) Machine Cycle Requirements from Page 167
c) Other Resource Consumption Requirements from Page 167
2. Dependability Requirements from Page 167
a) Accesability Requirements from Page 168
b) Availability Requirements from Page 169
c) Integrity Requirements from Page 169
d) Reliability Requirements from Page 169
e) Safety Requirements from Page 169
f) Security Requirements from Page 170
s839
3. Maintenance Requirements from Page 170
a) Adaptive Maintenance Requirements from Page 171
b) Corrective Maintenance Requirements from Page 171
c) Perfective Maintenance Requirements from Page 171
d) Preventive Maintenance Requirements from Page 171
4. Platform Requirements from Page 172
a) Development Platform Requirements from Page 172
b) Execution Platform Requirements from Page 172
c) Maintenance Platform Requirements from Page 172
d) Demonstration Platform Requirements from Page 172
5. Documentation Requirements from Page 173
8.9.2 Performance Requirements s840
Definition 77 –Performance Requirements: Byperformance requirementswe understand ma-chine requirements that prescribe storage consumption, (execution, access, etc.) time consumption, as well as consumption of any other machine resource: number of CPU units (incl. their quanti-tative characteristics such as cost, etc.), number of printers, displays, etc., terminals (incl. their quantitative characteristics), number of “other”, ancillary software packages (incl. their quantita-tive characteristics), of data communication bandwidth, etcetera.
s841
Pragmatically speaking, performance requirements translate into financial resources spent, or to be spent.
Example 98 – Timetable System Performance: We continue Example 86 on page 149. The machine shall serve 1000 users and 1 staff simultaneously. Average response time shall be at most 1.5 seconds, when the system is fully utilised. This ends Example 98
General s842 Till now we may have expressed certain (functions and) behaviours as generic (functions and) behaviours. From now on we may have to “split” a specified behaviour into an indexed family of behaviours, all “near identical” save for the unique index. And we may have to separate out, as a special behaviour, (those of) shared entities.
s843
Example 99 –Timetable System Users and Staff: We continue Example 83 on page 146 and Example 98 on the previous page. In Example 83 the sharing of the timetable between users and staff was expressed parametrically.
system(tt)≡client(tt)⌈⌉staff(tt) client: TT→Unit
client(tt)≡letq:Query in letv=Mq(q)(tt)insystem(tt)end end staff: TT→Unit
staff(tt) ≡
letu:Updatein let (r,tt′)=Mu(u)(tt)insystem(tt′)end end
s844 We now factor the timetable entity out as a separate behaviour, accessible, via indexed communications, i.e., channels, by a family of client behaviours and the staff behaviour.
type
CIdx /∗ Index set of, say 1000 terminals∗/ channel
{ ct[i]:QU,tc[i]:VAL|i:CIdx} st:UP,ts:RES
value
system: TT→Unit
system(tt)≡time table(tt) k(k {client(i)|i:CIdx})kstaff()
s845
client: i:CIdx→outct[i] intc[i] Unit
client(i)≡letqc:Queryinct[i]!Mq(qc)endtc[i]?;client(i) staff:Unit→outstints Unit
staff()≡letuc:Updateinst!Mu(uc)end letres =ts?instaff()end time table: TT →in {ct[i]|i:CIdx},st out{tc[i]|i:CIdx},ts Unit time table(tt)≡
⌈⌉
⌊⌋ {letqf =ct[i]?intc[i]!qf(tt) end|i:CIdx}
⌈⌉
⌊⌋let uf=st?in let (tt′,r)=uf(tt)ints!r; time table(tt′)end end
s846
Please observe the “shift” from using⌈⌉in systemearlier in this example to⌈⌉⌊⌋just above. The former expresses nondeterministic internal choice. The latter expresses nondeterministic external choice. The change can be justified as follows: The former, the nondeterministic internal choice, was “between”
two expressions which express no external possibility of influencing the choice. The latter, the non-deterministic external choice, is “between” two expressions where both express the possibility of an external input, i.e., a choice. The latter is thus acceptable as an implementation of the former.
This ends Example 99
s847
The next example, Example 100, continues the performance requirements expressed just above.
Those two requirements could have been put in one phrase, i.e., as one prescription unit. But we prefer to separate them, as they pertain to different kinds (types, categories) of resources: terminal + data communication equipment facilities versus time and space.
s848
8.9 Machine Requirements 167 Example 100 – Storage and Speed for n-Transfer Travel Inquiries: We continue Example 86 on page 149. When performing then-Transfer Travel Inquiry(rough sketch) prescribed above, the first
— of an expected many — result shall be communicated back to the inquirer in less than 5 seconds after the inquiry has been submitted, and, at no time during the calculation of the “next” results must the storage buffer needed to calculate these exceed around 100,000 bytes.
Storage Requirements s849
Machine Cycle Requirements s850
Other Resource Consumption s851
8.9.3 Dependability Requirements s852
To properly define the concept of dependability we need first introduce and define the concepts offailure, error,andfault.
s853
Definition 78 – Failure: A machine failure occurs when the delivered service deviates from