mplete and useful for mapping on another language. This type of refinement is pre-defined only for interface and behaviour descriptions (since textual representa- tion of collaboration structures is regarded a trivial tool issue). Figure 1.21 shows one important case: refinement of a state diagram, which translates the diagram into a set of textual specifications (called event specifications). Event specifications have a more detailed specification of states and transitions than is normally the case for a state diagram. START +asvScizeReq prel: hWfault prc2: congestic EXTERNAL EVENT -asvScizeRe +asvSeizeReg -asvSeize chScizeRequest(svId) PRECONDITION specification stl:{x <-logChanSet(svId) and oConnectReq/ inf refinement (Seize(confChanSet(x))+ Seize(twoPartyChanSet(x))+ Scize(idlcChanSct(x)) <32); This is a normal loSiczeReq/Cnt ACTIVITY digit receiver resGSSportTR +toneStartOrd STATE ERROR |stateErrorRepCnf( {cause "cardError"})} i:digit arrived -drDigitCi ACTIVITY FAILED loRcleaseReq/( 'nf resGSSportTR indigit arrive -drDigitCre |chSeizeRef(faultCode)) Fig. 1.21 Refining a state diagram to event specifications Another example of specification refinement is given in Fig. 1.22. This example shows refinement of an untyped specification of an abstract service primitive (ASP) to a typed one. In the typed specification, the names of parameters of the untyped specification are replaced by data types, the parameters are sequenced and formatting information and some extra identifiers may be added. 1 Introduction to Systems Modelling PRIMITIVE CAS/calInfoConfirm (CHOICE {Time, Day, Date}) Time ::= SET {hour,minute OPTIONAL} Day ::= {"Monday", "Tuesday", "Wednesday", "Thursday", "Friday", "Saturday", "Sunday"} Date ::= SET {month, day} specification refinement PRIMITIVE CAS/calInfoConfirm CHOICE {[0] Time, [1] Day, [2] Date}) Time ::= SEQUENCE {INTEGER SIZE (0..24),"." INTEGER SIZE (0..60) OPTIONAL} Day ::= IA5String {"Monday", "Tuesday", "Wednesday", "Thursday", "Friday", "Saturday", "Sunday"} Date ::= SEQUENCE {INTEGER