LIBRARY Michigan State Unlverslty PLACE IN RETURN BOX to remove this checkout from your record. TO AVOID FINES return on or before date due. DATE DUE DATE DUE DATE DUE use macs-ma INTEGRATING INFORMAL AND FORMAL APPROACHES TO OBJECT-ORIENTED ANALYSIS AND DESIGN By Yz'le Enoch Wang A DISSERTATION Submitted to Michigan State University in partial fulfillment of the requirements for the degree of DOCTOR OF PHILOSOPHY Department of Computer Science May 10, 1998 Advisor: Professor Betty H. C. Cheng INTEGR- ll l5 Clr'dlly mg}: the nwi where its cum of software. it :1 to rigort.)u.~l}' ( natatiuns HIP construct a ft tit"! r ‘ JILHFII Cdl 5‘ ABSTRACT INTEGRATING INFORMAL AND FORMAL APPROACHES TO OBJECT-ORIENTED ANALYSIS AND DESIGN By Yz'le Enoch Wang It is clearly evident that the impact of software is Significantly increasing. Accord- ingly, the need to have high assurance in software’s correctness increases for systems where its correct operation is imperative. As a means to facilitate the development Of software, formal software specifications are gaining increasing attention as a means to rigorously document requirements and design information Since the well-defined notations are amenable to automated processing for numerous analysis tasks, in- cluding verification of the correctness of resulting systems. However, attempting to construct a formal specification directly from an informal, high-level requirements document can be challenging. Formal descriptions potentially involve considerable syntactic details and may require careful planning and organization on the part of the developer in order to develop modular (easily-decomposed and amenable to reuse) Specifications. In contrast, object-oriented analysis and development techniques, such as the Object Modeling Technique (OMT), comprising diagramming techniques that 0,, . mitt use of '11:“; ': bdudaihnur l l v- ' A dhkmflwuxm_ repulse fortml. tex'eopment pr. u spatttatit._ttts the bitten levels of make use of intuitive and easy to understand graphical notations, are extensively used today. However, the informal nature of the diagramming notations and the lack of well-defined semantics pose the potential to introduce errors in the development process, particularly as the systems become more complicated. The objective of this research is to introduce formal semantics to the graphical notations of OMT, includ- ing a formal definition of their integration, and to propose a process to conduct a stepwise formal, rigorous refinement of the diagrams during the design phase. The development process should enable a semi-automated generation of executable formal specifications that can be used to simulate the behavior and check the consistency between levels of specification refinements. © Copyright May 10, 1998 by Yile Enoch Wang All Rights Reserved T0 my (lift to my 1 to my gra To my dear wife, whose companionship is a blessing from God; to my parents, who raised me to be a faithful Christian; to my grandparents, who shed their unconditional love on me. lat-hid Slnt‘t‘ft‘ll :1 rhcattIragerItettt atu rat to thank Dr. C Pijarrowslzi for tittrzmittre. lrotrld also 1 Chen. Gretel V. C in the Software l ‘riz-izrss in the p. finally. I trot; 331 must of all ( 75"” Mm, . “.5 forward I ACKNOWLEDGMENTS I would Sincerely like to thank my advisor, Dr. Betty H.C. Cheng, without whose encouragement and wisdom, this dissertation would not have been possible. I also wish to thank Dr. Philip K. McKinley, Dr. Anthony S. Wojcik, and Dr. Bryan C. Pijanowski for their constructive suggestions and commitment for being on my committee. I would also like to thank Gerald C. Gannod, William E. McUmber, Yonghao Chen, Gretel V. Coombs, Laura A. Campbell, Andrew S. Chen, and other members in the Software Engineering Research Group for all their friendship, support, and kindness in the past five years. Finally, I would like to thank my wife, Tong, for all her support, understanding, and most of all confidence in me. I appreciate the sacrifices She has made and am looking forward to more time together with her. vi lISI OF TABLE llSI OF FIGL'R 1 Introduction lPr-ohlern Dew l‘l SIIIrtItarx oil 3Defir3i Itiotts . . ‘54 Organization 2 Background 2.1 Object Rimle- 33 Formal .\lt7 ‘ l 13 S p(Illtdll'tfi 240 USjE‘tI .\.‘(J(lt 3 Related Wor ‘31 Jl FtJllli'dllZ [dih- 97 ‘ 1* -\Jll~ ”OlJJi‘i'P' 33 c . . o_5[tr1a1 l( - 4 Object Mod. TABLE OF CONTENTS LIST OF TABLES x LIST OF FIGURES xi 1 Introduction 1 1.1 Problem Description and Motivation .................... 2 1.2 Summary of Research Contributions .................... 4 1.3 Definitions ................................... 6 1.4 Organization of Dissertation ......................... 7 2 Background 8 2.1 Object Modeling Technique Overview .................... 8 2.2 Formal Methods ............................... 12 2.3 Specification Languages Used in Project .................. 18 2.4 Object Model Formalization ......................... 21 3 Related Work 30 3.1 Formalization of Object-Oriented Modeling Approaches .......... 30 3.2 Non-Object-Oriented Based Approaches .................. 49 3.3 Systematic Approaches to Refinement of Analysis Information for Design 55 4 Object Model Formalization Revisited 60 4.1 The Derivation of Algebraic Specifications ................. 60 4.2 Distinguished Sort .............................. 61 4.3 An added formalization rule ......................... 62 4.4 Formal Representation of Algebraic Specification ............. 65 5 Dynamic Model Formalization 67 5.1 Preliminary Formalization .......................... 68 5.2 Formalizingstate diagrams of individual objects .............. 71 5.3 Concurrent State Formalization ....................... 86 5.4 Integration with Other OMT Models .................... 94 5.5 Summary ................................... 98 6 Functional Model Formalization 99 6.1 The Data Flow Diagram (DFD) ....................... 101 6.2 DFD Notation Modification ......................... 103 6.3 Integrating the Functional Model into OOD ................ 110 vii i. 'I‘ '1 l 61 Fllllt‘llttlldl .\I.. It.) lit-.3193 atltII‘I \3‘3' .36 Summary 7 Model lutegr: 7.1 Integratiun of 7.3 The Corretrtt. .3 I. Spti‘lfitdltul. 71 Analysis of .‘I 8 Design Proce ‘l O'I'E‘l'l'lflt' Ui- iil IhePrI'mt-sr 5.3 The Design 3.4 Summary 9 Case Study 9.1 The Project 7 Focus of th. 3 Overview o: l 3 '1'. 9'. ‘1 3 System 1.3 5}'Stem De: Design Ana Summary 9 93 '3.‘ 19 Conclusion it} . «1 Summary I 23.2 I ' Impact ()f ' BIBLIOGRA‘. viii 6.4 Functional Model Formalization ....................... 116 6.5 Integration with Object and Dynamic Models ............... 145 6.6 Summary ................................... 146 7 Model Integration and Analysis 147 7.1 Integration of the Three Models of OMT .................. 147 7.2 The Correctness, Consistency, and Completeness of the Formalization Rulesl51 7.3 Specification Analysis Techniques ...................... 153 7.4 Analysis of Model Integration ........................ 158 8 Design Process 165 8.1 Overview of Strategies Proposed Approach ................. 168 8.2 The Proposed Rigorous Design Process ................... 171 8.3 The Design Process Applied to An Example ................ 178 8.4 Summary ................................... 206 9 Case Study 209 9.1 The Project .................................. 210 9.2 Focus of the Case Study ........................... 213 9.3 Overview of the Requirements Analysis ................... 213 9.4 System Level Modeling ............................ 215 9.5 System Design ................................ 225 9.6 Design Analysis and Refinement ....................... 245 9.7 Summary ................................... 267 10 Conclusions and Future Investigations 269 10.1 Summary of Contributions .......................... 270 10.2 Impact of Research and Future Investigations ............... 273 BIBLIOGRAPHY 276 APPENDICES 284 A The Object Model Formalization Rules 284 B The Dynamic Model Formalization Rules 286 C The Functional Model Formalization Rules 291 D Complete LOTOS specification for Disk Manager Behavior 296 E Instantiated LOTOS specification for Disk Manager 299 F LSL specifications 301 G LOTOS specification for revised Disk Manager 303 H Complete LOl ix H Complete LOTOS specification of EN FORMS for static analysis 306 3.1 The models t LIST OF TABLES 8.1 The models that will be developed during a given iteration of design . . . 173 l .A 111611131111} 5 13 A generlt‘ til; 3.3 .An (.Iperat It 3.1 .A dt’lll.rldllHI 2.3 A Larch alIv 3.6 .A typical L(. ..I BasiIC ap 1TH; 2.5 HIgh-lexil 5t .ASIII'Iple I31. 111. The Corn» \‘Y , 3113mm cm 11 31'. Sun mar} II -\.J ~13 ASIIIIIIEE" 31., 214 .Ahtgh luv 15 .eAhi g-h 1+th Iv The ACT ( A Sample 5 he 3mm; medal 41 A? 43 A 111110131 5 'A t‘ph'dl 5 The State. A C07] 7 5.1 3.? 5.3 5.1 r: )3 The Std? (I 73.1 T11; ‘pft J5 A San};1 39f I“ d n , . TAII' 3‘1 Spp(lfi(ae 3.153 , ‘ -. . l~ SdUlplp SI 5.} r 3 ill-Ural 1‘ r I t“) ‘ 31:3,; "J l LIST or FIGURES 2.1 A predicate specification of integer square root ............... 14 2.2 A generic algebraic specification of stack .................. 15 2.3 An operational specification of integer square root ............. 16 2.4 A denotational specification of boolean expression ............. 18 2.5 A Larch algebraic specification of table ................... 19 2.6 A typical LOTOS process algebra specification ............... 21 2.7 Basic approach to formalization ........................ 22 2.8 High-level structure of LSL specifications .................. 23 2.9 A simple object model ............................ 25 2.10 The corresponding algebraic specification of Figure 2.9 .......... 25 2.11 Summary of Object Model Semantics .................... 26 2.12 Summary of Object Model Semantics (continued) ............. 27 2.13 A simplified disk manager .......................... 27 2.14 A high-level Storage class specified in Larch ................ 28 2.15 A high-level Storage class specified in ACT ONE ............. 29 4.1 The ACT ONE Specification for person .................. 63 4.2 A sample object model that contains attributes for object O ....... 64 4.3 The automatically generated formal specification from the sample object model ................................... 65 5.1 A typical statechart .............................. 70 5.2 A typical state diagram ........................... 72 5.3 The state diagram for the Compressor object ............... 78 5.4 A Compressor class and its behavior specified in LOTOS ......... 80 5.5 The state diagram for Storage ........................ 83 5.6 The specification (in Full LOTOS) of the Storage (1) ........... 83 5.7 The specification (in Full LOTOS) of the Storage (2) ........... 84 5.8 A sample state diagram with interleaving dynamic models ........ 88 5.9 The aggregation concurrent state diagram for Disk Manager ....... 91 5.10 The LOTOS specification for a simplified Disk-Manager ......... 92 5.11 Specification for a simplified Disk_Manager with hidden internal gates . . 93 5.12 Sample state diagram with instantiated parameters of distinguished sorts 95 5.13 LOTOS specification of the sample state diagram ............. 96 6.1 A typical data flow diagram ......................... 101 6.2 An OFM that contains services of an individual object .......... 105 6.3 An OFM of an integer stack object ..................... 105 xi 6.1 A system level 6.3 AII 313151 >1.II‘~' 5131111115 116 .All 8131:.“ 111;! 6.7 An $13151 \\“.t' 6.3 An 513111 wit 119 81519111 1e\‘e1 1. 5.111 A simplified I1 6.11 The 0111 for 6:13 The 0151 hr 513 The 311131 1« 6.11 The ACT (‘13 6.173 The ACT (15 6.16 The Full 1.11" nuns and 6.1". The Full LU 110115 101 : 5.15 A typical 51:“: 6.19 A pan of 11}. 530 The forumliz 6.31 The form-£1111 6.32 The Full U; 101 8(3th 1133 The Full LC 110113 for 6.34 The 1.81. spe 625 The Proof 01 I1 The finrruat n‘) ‘ I. he error II. ..3 .e testing II sing am *1 is) An exhausri I6 .11 interacti 51 T1113 1.0771111 .1") ; Models in I1 K . {I The sysiezu ;1 The ACT 0' :"J The S‘A.“("I'1 .535 TI 1 1 3 .Ie “ - ; ~ ‘ «513(f UH me ~. “ ‘ ~ Ir-m 33 I; 1.23;: ‘1 a 11" “N i xii 6.4 A system level OF M derived during analysis ................ 107 6.5 An SRFM shows how a system service is implemented in terms of object services .................................. 108 6.6 An SRF M that introduces an additional internal function ......... 108 6.7 An SRF M with split and aggregate data flows ............... 109 6.8 An SRFM with refined input and output data flows ............ 110 6.9 System level object functional model for Disk Manager .......... 112 6.10 A simplified disk manager .......................... 113 6.11 The OFM for Storage ............................. 113 6.12 The OFM for Compressor .......................... 114 6.13 The SRFM for Disk_Manager.Retrieve ................... 114 6.14 The ACT ONE specification for Disk Manager ............... 119 6.15 The ACT ONE specification for Storage .................. 120 6.16 The Full LOTOS specification for Disk Manager with algebraic specifica- tions and distinguished sort ....................... 123 6.17 The Full LOTOS specification for Disk Manager with pre- and postcondi- tions for services ............................. 126 6.18 A typical state diagram ........................... 128 6.19 A part of the refined ACT ONE specification for Disk Manager ..... 135 6.20 The formalization of the refined data items shown in Figure 6.7 ..... 139 6.21 The formalization of the data duplicator and selector shown in Figure 6.8 141 6.22 The Full LOTOS specification for Storage with pre— and postconditions for services ................................. 143 6.23 The Full LOTOS specification for Compressor with pre- and postcondi- tions for services ............................. 144 6.24 The LSL specification for the refined Disk Manager ............ 144 6.25 The proof of the example constraint using LP ............... 145 7.1 The format of formal specifications ..................... 149 7.2 The error in the behavior specification of the Storage detected by LSA . 158 7.3 The testing process used to test the behavior of Disk Manager ...... 160 7.4 Using accept_test testing process to test the specified Disk Manager . . . 161 7.5 An exhaustive test using process accept-test ................ 162 7.6 An interactive simulation of the process composed for testing ....... 164 8.1 The formalization process dimension of the suggested framework ..... 169 8.2 Models in the order of development ..................... 174 8.3 The system object model for Disk Manager ................ 179 8.4 The ACT ONE specification for system level object model of Disk Manager179 8.5 The system functional model for Disk Manager .............. 181 8.6 The specification for Disk Manager that specifies its services and propertie8182 8.7 The system dynamic model for Disk Manager ............... 182 8.8 The complete Full LOTOS specification for system level object model of Disk Manager ............................... 183 8.9 The testing process used to analyze the behavior of Disk Manager . . . . 184 H11 15111g1211r’.- 111111? 1111111151 11'. 8.7;? The ACT ON 5.13 The objmjt 111 3.11 The ohjeei (1A 5.1-5 The 5111311111 11? 5.15 The 51113111111. .1‘ 3.7... The object 11.: 3.15 The ohjeet I1 5.9 T119 Spuihzd 5.311 An exaIIIII‘II- 5.31 The service I 3512 The service r 5.33 The refi'II-I-Iil 5.31 The 151. 5;» 3'1? The proof 0: An example .AII exarII Ip‘o AII exarup ml The refi 1111 The {9115011 The 191; '111‘1 J (' .1“) 1 ‘1?) Jr) 3’) ‘ 1”. . - II.) (”p I.) 0—) V (.9 w (I) All The 11111111 11 (111181111 II -l (:3 (I Q (”PA (I‘ SA 551111; (Mr (_ IigI‘I-lm . 119 (19:51; :3 The form he fauna 97 he trans 0; check I .5 The trans r for sin n he fIIrII F” eonrlii' 7;. .A test p. H The tram 8.10 8.11 8.12 8.13 8.14 8.15 8.16 8.17 8.18 8.19 8.20 8.21 8.22 8.23 8.24 8.25 8.26 8.27 8.28 8.29 8.30 8.31 8.32 8.33 8.34 8.35 9.1 9.2 9.3 9.4 9.5 9.6 9.7 9.8 9.9 9.10 xiii Using accept_test testing process to analyze the specified Disk Manager . 185 The refined object model for Disk Manager ................. 189 The ACT ONE specifications for object models of Storage and Compressor 189 The object functional model for Storage .................. 190 The object dynamic model for Storage ................... 191 The specification for object Storage in Full LOTOS ............ 192 The specification for object Storage in Full LOTOS ............ 193 The object functional model for Compressor ................ 194 The object dynamic model for Compressor ................. 194 The specification for Compressor in Full LOTOS ............. 195 An example refined object model ...................... 196 The service refinement functional model for function Input of Disk Manager196 The service refinement functional model for function Output of Disk Manager197 The refined ACT ONE specification for Disk Manager ........... 197 The LSL specification for the refined Disk Manager ............ 198 The proof of the example constraint using LP ............... 198 An example dynamic model for object 0 .................. 200 An example SRF M for service S 1 of object O ............... 200 An example refined dynamic model for object O .............. 201 The refined dynamic model for Disk Manager ............... 202 The revised refined dynamic model for Disk Manager ........... 202 The refined ACT ONE specification for Disk Manager ........... 203 The refined dynamic model for Disk Manager that is composed by parallel dynamic models .............................. 205 The composed specification for Disk Manager ............... 205 Using accept_test testing process to analyze the behavior of the refined Disk Manager (1) ............................. 206 Using accept-test testing process to analyze the behavior of the refined Disk Manager (2) ............................. 207 A high-level view of the architecture .................... 212 The design models of EN FORMS at the system level ........... 216 The formal specification automatically generated from system models (1) 217 The formal specification automatically generated from system models (2) 218 The transcript of running LSA over EN FORMS formal specification to check inter-model consistency ...................... 219 The transcript of running LOLA over ENFORMS formal specification for simulation ............................... 220 The formal specification with algebraic specifications and pre/post- conditions ................................. 222 A test process for the refined formal specification of ENFORMS . . . . 223 The transcript of testing that runs OneExpand of LOLA over the refined EN FORMS formal specification .................... 224 The transcript of testing that runs TestE'zpand of LOLA over the refined ENFORMS formal specification .................... 226 9.11 Th9 {093111199 1191: 9.1“} The (11.351111 1111 11 9.13 The 31111111111111.1- 914 The formal 11pm pre 'p11~‘1~1‘-.1 9.13 The design 1111- 9.16 The “1111;111:1111 93.1- The 31111111111119! 9.15 The {111111111 1;: and pro; 11 99T1ed1\"1111; 9.3“ T16 31111111 9.31 The 2111111111213 932 The formal . PT? 'lme-1 :33 The SRHT 1'1 31 The 2111111111;1 93-3 The refined 1f 9135 The 131111111111" modeT of :3; T9: d3~'ne1111i1 ' aUILJIli‘i' STEHTS 1n 9‘3 Th9 r1 finpd 9111Thed1<1znr 31The 21111311111 Of CIIU'T" 3:21 The rexiwd . 3 The 21111111111 1'1? behax'i1'1r - qvntzn'c (TINT W ifieation :—--1 sing expa 9F ' u part of t‘ W pendix I «~‘Jl 9311 3 “51“ d 93C! 6 TUHIAT zetranser 91"» T9 13 refinu p 9 119 {PC :‘ C ”at [1n r. ‘ UTHI‘HIJV ‘ .112 T5 1 1 :1. FIT‘T. IJIW ‘1': OP‘ I1 3 313 d“ ' 9 .3 .. dr4|4f1(j ' 9.11 9.12 9.13 9.14 9.15 9.16 9.17 9.18 9.19 9.20 9.21 9.22 9.23 9.24 9.25 9.26 9.27 9.28 9.29 9.30 9.31 9.32 9.33 9.34 9.35 9.36 9.37 9.38 9.39 9.40 9.41 9.42 9.43 xiv The refined object model for ENFORMS: an overview of the architecture 228 The design models for Name_Server ..................... 229 The automatically generated formal specification for Name_Server . . . . 230 The formal specification for Name-Server with algebraic specifications and pre/post-conditions ............................ 231 The design models for Archive_Server .................... 232 The automatically generated formal specification for Archive Server ( 1) . 233 The automatically generated formal specification for Archive Server (2) . 234 The formal specification for Archive-Server with algebraic specifications and pre/post-conditions ......................... 235 The design models for Client ......................... 236 The automatically generated formal specification for Client ........ 237 The automatically generated formal specification for Client ........ 238 The formal specification for Client with algebraic specifications and pre/post-conditions ............................ 239 The SRF M for Retrieve service of ENFORMS .............. 240 The automatically generated formal specification for the SRFM of Retrieve 240 The refined design model for ENFORMS ................. 241 The automatically generated formal specification from the refined dynamic model of ENFORMS .......................... 242 The dynamic models composed in parallel ................. 244 The automatically generated formal specification that describes the con- stants in the refined models of ENFORMS .............. 246 The refined object model for EN FORMS with Channel object ..... 248 The design models for channel ........................ 248 The automatically generated formal specification from the design models of Channel ................................. 250 The revised design models (with a Channel object) composed in parallel 251 The automatically generated formal specification that synchronizes the behavior of individual objects ...................... 253 Syntax checking and semantics analysis of the refined enforms formal spec- ification .................................. 254 Using expansion transformation to detect synchronization error ..... 255 A part of the EFSM transformed from the LOTOS Specification in Ap- pendix H .................................. 256 The refined dynamic model of Client .................... 257 The formal specification for the refined Idle state of Client ........ 258 The transcript of expansion transformation after the behavior of the Client is refined .................................. 258 The test process for the refined formal specification of ENFORMS . . . 259 Communication among individual objects are hidden ........... 260 The test process is rejected by the refined behavior specification of EN- FORMS .................................. 261 The added operations and equations that are resulted by the SRFM of Figure 9.23 ................................ 262 9.44 The trarrsrripr r are addml 94.3 The further rr-fi 9.46 The hirmal an 9.4? The result oi T refined . . XV 9.44 The transcript of Testhrpand test after necessary operations and equations are added ................................. 263 9.45 The further refined dynamic model of Client ................ 265 9.46 The formal specification for the refined Idle state of Client ........ 266 9.47 The result of TestExpand after the behavior of the Client object class is refined ................................... 267 Chapter Introdu< it E clearly evidcr: trniingi}: the rim: S'stems Where its in; increasing am ntairrriation since {Oi numerous and ~3>iEnis. Haiufm'v inf [V‘T ' i . J mal. hlgirlf‘t [flip ”U. . ' ,2 mail} lllVUlV- Off”. ' ' Wildliiiin on Y Chapter 1 Introduction It is clearly evident that the impact of software is significantly increasing [1]. Ac- cordingly, the need to have high assurance in software’s correctness increases for systems where its correct operation is imperative. Formal specifications are gain- ing increasing attention as a means to rigorously document requirements and design information since the well-defined notations are amenable to automated processing for numerous analysis tasks [2], including verification of the correctness of resulting systems. However, attempting to construct a formal specification directly from an informal, high—level requirements document can be challenging. Formal descriptions potentially involve considerable syntactic details and may require careful planning and organization on the part of the specifier in order to develop modular specifications. 1.1 PI‘OblCI .l rnrrplernurrtary a; in; irritations. F ii r 7. used as a pupular t ' taught as an alijm-n largely due to its >i: and. behavioral. at; inc functional tnmli similar to entity-ruin ofastatediagrarn. . {trier t0 ellectiwly 1 defined method to it u; :nree separate. in {hill may help to (‘i One approarlt ti 3:J‘flht'ation5: and ' CrLILS Q trim a “rim at; Pi'i'x'" “ ' -rrng speciiit' Mall-303061] as l 'C-nr': 1 H‘JEYIES. d(¢"( ,. l ;_ l'. “-.;‘.‘.*.’li’ -‘ ‘ mildllUH rulv \ i" safer t" “ was. illiljij' 2 1.1 Problem Description and Motivation A complementary approach to describing requirements is the use of graphical model- ing notations. For example, the Object Modelng Technique (OMT) [3] is extensively used as a popular object-oriented modeling technique in industry and is commonly taught as an object-oriented methodology in academic settings. Its popularity is largely due to its simple notation and the notational support for describing struc- tural, behavioral, and functional aspects of a system through the object, dynamic, and functional models, respectively. The object model is represented in a notation similar to entity-relation (ER) diagrams [4]. The dynamic model is described in terms of a state diagram. And the functional model is captured by a data flow diagram. In order to effectively use OMT, particularly for design purposes, there must be a well- defined method to integrate the three models. Otherwise, OMT is only a combination of three separate, independent models that provide little more than intuitive diagrams that may help to clarify some ideas within the corresponding, separate models. One approach that takes advantage of the automated processing afforded by formal specifications and the ease of use provided by graphical modeling techniques is to construct a well-defined syntax and semantics for the graphical models in terms of an existing specification language. A significant advantage to formalizing a modeling notation such as OMT is that it has a uniform notational support for modeling requirements, design, and detailed design information. Therefore, the corresponding formalization rules for diagrammatic models can be used to perform analysis and design tasks throughout the development process, rather than be limited to a specific phaét? dig” require II; :3_.:tiriillg notatiuns Huttever. Stilli?’ l ge'trait speeihra: it i: fahngin. Thus full; furthermore. the l resulting models. l tian of the formal nni‘els. from \Vlllt‘ he: Approach The and refinement 0f 5:»: graphical not a Thesrs Stateme {gig-p formal .5755? TN] for the rec Wining Qittli? - ,Rv‘ :_ 17 .156 a re . ' Lu objeryg- a.” ,p r ,. 41" .. flu-{l 7r ‘ 11 (Odfi- 5‘ t B P {:e. '4";‘5m€nt 3 phase (e.g., requirements), as is the case with numerous specification languages and / or modeling notations. However, some features of the formal specifications, such as the equations in a1- gebraic specifications, cannot be represented by graphical notations in an intuitive fashion. Thus fully automated generation of formal specifications is not realistic. Furthermore, the formalization rules can only derive formal specifications from the resulting models, but cannot help to conduct the development process. The applica- tion of the formal specifications may be limited by the fact that their corresponding models, from which the specifications are generated, are derived in an informal, ad hoc approach. Therefore, a process that supports a formal and rigorous development and refinement of analysis and design information with the use of formal semantics for graphical notations is necessary. Thesis Statement: The objective of the proposed research is threefold: (1) de- velop formal syntax and semantics for all three OM T models; (2) develop a formal definition for the integration of all three models; and (3) develop a refinement process for refining analysis information into design information. These three tasks will de- fine a new object-oriented design paradigm that supports rigorous analysis of 0M T’s graphical models through specification execution, consistency verification, and stepwise refinement. 1.2 Summit Th5 section give in Formalization of dynamic intuit-ls in 1 page of Tetnpt ital an individual Ulljl“ the state diagram The state diagram. s’tthranized LOT ratification of lllt executable sperili Formalization C no tiihject-orierrt flint"? . ._tlt)naJ “10‘“ ~. . “‘ ‘1 “eta! .llot'F-l .32 V‘ -. - ll l'J'h‘erzt An snr tlif: (on? v\ 1 ' ' (‘3‘ prot- '« nrn - “5 fur derir'i n ; rit- snfi , B d.\.(d ”l“ 4 1.2 Summary of Research Contributions This section gives highlights of the four major contributions of this research. Formalization of Dynamic Model. New rules are proposed to formalize the dynamic models in terms of process algebra specifications expressed in LOTOS (Lan- guage of Temporal Ordering Specification) specifications. In OMT, the behavior of an individual object is modeled as a state diagram. The proposed rules formalize the state diagrams for individual objects in terms of LOTOS behavior specifications. The state diagrams of concurrent, communicating objects are formalized in terms of synchronized LOTOS behavior specifications. The formalization enables the precise specification of the behavior of objects and the simulation of system behavior through executable specifications. Formalization of Functional Model. In order to integrate the functional models into object-oriented technology, the functional model of OMT has been modified. Two functional models, Object Functional Model (OFM) and Service Refinement Func- tional Model (SRFM), are introduced. An OFM captures the services provided by an object. An SRF M describes how a service of an object is implemented in terms of the services provided by the object at a lower level of abstraction. In addition, guide- lines for deriving algebraic specifications from the object and functional models are given. Based upon algebraic specifications, pre- and postconditions are introduced to describe the requirements and constraints for services. The pre- and postconditions of services enable symbolic execution of the high-level design model thus providing a means to perform ~.~ situate derelupnn-t integration of tin three trrntp‘nétrn'n‘ A13 re derived in lilt' t aritnamic model 1 the models with r' negation is awhi- Ltaiization rules. derived from the t sated and retirees. liathiet'ed by («m according to the Dian object if , - 1 ft The integrat i« CI" v.1?» me‘emi’lliarv .. . c f”mil ~ . mffi‘rfifd, i‘l’l ‘, “ii in ‘u means to perform simulation, verification, and validation during the early phases of software deveIOpment. Integration of the Three Complementary Models. The integration of the three complementary models is three-fold. First, the functional and dynamic models are derived in the context of object models. By associating a functional model and a dynamic model to every individual object, the conflicts can be resolved between the models with respect to their respective development philosophies. Second, the integration is achieved through the underlying formal semantics imposed by the for- malization rules. By sharing common language constructs among the specifications derived from the object, functional, and dynamic models, the three models are inte- grated and represented in terms of a single formal specification. Third, the integration is achieved by composing: (1) the dynamic models of concurrent objects hierarchically according to the system structure specified in the object model; and (2) the SRFMs of an object in terms of the services provided by the aggregate objects. The integration and formalization of the three models that describe a system from complementary aspects enable designers to perform analysis tasks by using the derived formal specifications. In addition, based upon the formalization and integration, a design process that incorporates formal specifications in a transitional, parallel successive refinement approach [5] is also possible. Process for Model Construction, Specification, and Refinement. Based on the investigations into the formalization and integration of the models of OMT, a lazgn process, 15 pr uparallel with the of the rigorous ilia' and designers ran it | anhiguities. in midi understand the am even with the rust ,. model refinement t: ea'ner stages of ml v . 1'3 Defini 51.??? our researrh as. it 18 import; .isene}: and can: on Va '~ allluns apply- 0 Correct me ““1 Still he Ill ' C 0 . Q ‘- - “en design process is proposed to facilitate the development of formal design specifications in parallel with the development of OMT’S semi-formal, graphical models. Because of the rigorous mathematical foundation of formal specifications, both customers and designers can have a more precise means to describe the design thus avoiding ambiguities. In addition, symbolic simulation of the design can help designers better understand the design as well as facilitate the communication among designers and even with the customers. And finally, specification analysis can be performed during model refinement of the design process to detect and eliminate design flaws during earlier stages of software development. 1 .3 Definitions Since our research focuses on the application of formal methods and the design pro- cess, it is important for us to clarify what we mean by the terms correctness, con- sistency, and completeness. These terms have been given different meanings based on various perspectives [6, 7], but for the remainder of the dissertation, the following definitions apply. 0 Correctness: after a refinement of a service, the postcondition of the services can still be satisfied. 0 Consistency: the formal specifications derived from the models (1) do not have syntactical and semantic errors, (2) do not have deadlocks among concur- rent, communicating objects, and (3) the test cases that are satisfied by the design specification of a higher level abstraction can still be satisfied after one refinement iteration. o Completeness: the formal specifications describe all the required functionali- ties as well as the behavior of the system under all circumstances. 1.4 Organl The remairnler ml ll! fifth]; Oi)]€t.‘l .\ir nit’ gaggigges that will the object model u‘ ter 4 revisits the t nation rule. Chap in terms of the U malel into ohjm-t- functional models. El‘ we integrated the enrreSporn‘lirr; and to perfartri s; ”ill-”LS a Stepwise : Si’t‘v‘i'iheations. C lib-39933 l0 3 lay-LI, LI 7 1.4 Organization of Dissertation The remainder of this dissertation is organized as follows. Chapter 2 gives an overview of the Object Modeling Technique (OMT), formal methods, the formal specification languages that will be used, and preliminary investigations into the formalization of the object model of OMT. Chapter 3 discusses work related to this research. Chap- ter 4 revisits the object model formalization and introduces an additional formal- ization rule. Chapter 5 describes the formalization of the dynamic model of OMT in terms of the LOTOS specification language. Chapter 6 integrates the functional model into object-oriented technology and discusses the formalization rules for the functional models. Chapter 7 discusses how the object, functional, and dynamic mod— els are integrated in terms of their underlying formal semantics. It also discusses how the corresponding specifications can be used to simulate the behavior of the system and to perform specification analysis. Chapter 8 proposes design process that con- ducts a stepwise refinement of design by using the diagrammatic models and formal specifications. Chapter 9 describes a case study that applies the proposed design process to a large-scale project, EN FORMS. Chapter 10 gives the conclusions and discusses future investigations. Appendices A through H give complete formalization rules and formal specifications generated from OMT models. Chapter Backgro This thapt er preset lSOVEN'ieWEd. lllt‘l l :it'el}: Next. the E r, l l ital}: the lorrrra 2.1 Objec TL, "- ' .ne Uhjf‘Ci .llodi . :33” ' ' ' - n3, to fatrrlite ?" - I; :r r ' te diagrarrrrnir. Chapter 2 Background This chapter presents background material relevant to the dissertation research. OMT is overviewed, including how it is used during the analysis and design phases, respec— tively. Next, the specification languages Larch and LOTOS are briefly introduced. Finally, the formalization of the object model is overviewed. 2.1 Object Modeling Technique Overview The Object Modeling Technique (OMT) is a methodology developed by Rumbaugh, et al [3], to facilitate object-oriented analysis and design (00A and OOD). It includes three diagramming techniques to describe different aspects of a system. 2.1.1 Complementary diagramming techniques The essence of the Object Modeling Technique is to build a model of an application domain during the analysis of a system that can be augmented with implementation legals during the ii sheet model. dg'urr'. ii a system. ERl‘ll tr implementation «let. [be gibjett diazranfi Object Model. tutld that is impr three diagrams. lt their relationships it is straightlortt‘a The object diagra made-ls are based. that can be \‘alua‘ SITE llle diagram-a Sent classes: line». if association lint relief" .-.lull>lrl] )SI trip Dynamic Mode 1115‘: the beha '3- i L65"? - .. “5rd I Q] details during the design phase. The modeling consists of three orthogonal models, object model, dynamic model, and functional model, each depicting different features of a system. Each model is applicable during all stages of development and acquires implementation detail as the development progresses. The models are represented as the object diagram, state diagram, and data flow diagram, respectively. Object Model. An object diagram is used to capture information about the real world that is important to an application. Thus it is the most important of the three diagrams. It describes the static objects in a system by showing their identity, their relationships to other objects, their attributes, and their operations. Therefore, it is straightforward to derive abstract data types (ADT) from the object diagrams. The object diagram forms a basic framework upon which the dynamic and functional models are based. The diagram provides an intuitive visual representation of a system that can be valuable in the communication between the customers and the developers since the diagrams serve to document the structure of a system. In OMT, boxes repre- sent classes; lines between boxes represent associations; empty, solid circles at the end of association lines represent different multiplicities; diamonds represent aggregation relationships; triangles represent inheritance relationships. Dynamic Model. A state diagram graphically represents the dynamic models that describe the behavioral aspects of a system concerned with events, time, and changes. Each state diagram depicts the state and event sequences allowed in a system for one class of objects. The notation used for dynamic models is a variation of Harel’s StaIet‘hart noration transitions. ln (llll events that trineer diagrams. Punt-tit a: diagram: operation: functional .\lod grams is the lililt Data flow diagram and data flows. r the operations in artistraints for \‘a 2.1.2 Requ in GMT. the oh i (7.".4 . l . Ere aspects of [in .. ' mat-tic model I r . . lifier n ‘dll. ' - dlt Dill-J] “ l. P dam («is . {HUT-Ff 5,. 10 Statechart notation [8], where ovals represent states; arcs with arrows represent state transitions. In OMT, rounded rectangles represent states; labels on arrows represent events that trigger state transitions. State diagrams also reference the other OMT diagrams. Functions in a data flow diagram correspond to the actions from the state diagram; Operations on objects in the object diagram are modeled as events in a state diagram. Functional Model. The functional model, depicted in the form of data flow dia- grams, is the third dimension of the three orthogonal modeling techniques of OMT. Data flow diagrams (DFD) consist of nodes and arcs, which correspond to processes and data flows, respectively. The data flow diagram also specifies the meaning of the Operations in the object model and the actions in the dynamic model, as well as constraints for values within an object model. 2.1.2 Requirements Analysis In OMT, the objective of requirements analysis is to devise a precise, concise, un- derstandable, and correct model of the real-world [3]. The analysis models describe three aspects of objects: static structure (object model), sequencing of interactions (dynamic model), and data transformation (functional model). The object model describes real-world object classes and their relationships to each other, and it should be the first model to be derived from a problem statement because the static structure of a system is usually better defined, less dependent on application details, more stable as the solution evolves, and easier for humans to understand. During the analysi~ and operations. arv prepared: inherit. ohjeet model at the and refinements. The dynamic tn «*i‘tieets. it is the s or more scenarios. ' eternal display for include all signals. has-d upon the st: diagram. which ie event flow diagra: ”litigant for each tier.“ . . "*5 the Object 53. a1} . ~ eient fit iW di The function; noat consider .Lut laerg -‘ ( ‘ .ii 11 During the analysis phase, modeling entities, such as classes, associations, attributes, and operations, are identified; a data dictionary that contains all modeling entities is prepared; inheritance relationships between object classes are identified. The final object model at the end of the analysis phase is obtained through repetitive iterations and refinements. The dynamic model shows the time—dependent behavior of the system and the objects. It is the second model to be derived during the analysis stage. Initially, one or more scenarios (a scenario is a sequence of events) that show the major iterations, external display formats, and information exchanges are prepared. The events, which include all signals, inputs, decisions, interrupts, transitions, and actions, are identified based upon the scenarios. And each scenario is described in terms of an event trace diagram, which is an ordered list of events between different objects. In addition, event flow diagrams that depict events between classes are derived. Finally, a state diagram for each object class with nontrivial dynamic behavior that describes the events the object receives and sends is obtained based upon the event trace diagrams and event flow diagrams. The functional model that shows data dependency and how values are computed without considering sequencing, decisions, or object structure is the last model to be derived. In OMT, similar to the process used in structured analysis, input and output values of the system are first identified. A top level data flow (DFD) diagram is developed according to the input and output values. Then each nontrivial process is recursively expanded into a low-level DFD until every process corresponds to a function. A description for each function, which can be in natural language, math- entatit‘al {’Qllalltth‘ once the DP D has 2.1.3 Desigt' 0}le decomposes System Design. guidelines for the this Stage. object isto provide. co tasks. decisions 3f? made. The i flit ‘ ....:n the attatys W to be i re.» . «adg This St. fill r‘r . 12 ematical equations, pseudo—code, or some other appropriate form, should be written once the DF D has been refined to a sufficient level of detail. 2.1.3 Design OMT decomposes the design phase into system design and object design stages [3]. System Design. The objective of the system design stage is to establish high-level guidelines for the object design and to make global decisions concerning the design. In this stage, objects are grouped into subsystems according to services that the system is to provide, concurrency is identified, subsystems are allocated to processors and tasks, decisions about data store management and software control implementation are made. The implicit presumption of all these activities is that the models obtained from the analysis phase are sufficiently detailed to contribute to this phase. Object Design. During the object design, decisions about how the classes are going to be implemented according to the strategy chosen during system design are made. This stage includes determining the data structure of attributes, algorithms for operations, association design, and addition of internal objects, and so on. 2.2 Formal Methods A formal method is characterized by a formal specification language and a set of rules governing the manipulation of expressions in that language. A formal specification language provides [9]: o a synthetic d o a Sfrttunt‘tt‘ (I o a satt.~'f.rrtt~t. tintpletnent } Turtnal spet‘ilit a ‘ analysis results at. eret‘ntion :111 (’Xt't". steps {refinements There exists in; can be partitioned fictitious are cornxt denotational. 2'2‘1 AXiOn‘. The Grit/mam 3:: ”TEL-T ' F rlllt‘bg Of “T 7. 4 ll ‘1 ‘ 11 1 dldCIlldllCdl l1] h‘_:'.1 pdhlde My», a ffjr It 13 o a syntactic domain: the notation in which the specifications are written. 0 a semantic domain: a universe of elements that may be specified, and o a satisfaction relation: indicates which elements in the semantic domain satisfy (implement) which specifications in the syntactic domain. Formal specifications can be checked by tools that help explore the consequences of analysis results and design decisions [2], detect logical inconsistencies [10], simulate execution [11], execute symbolically [12], and prove the correctness of implementations steps (refinements) [13]. There exists many types of formal specifications. Formal specification languages can be partitioned according to a high-level classification [14]. The formal speci- fications are commonly categorized into three classes: axiomatic, Operational, and denotational. 2.2.1 Axiomatic specifications: The axiomatic approach to specification implicitly defines the semantics of a pro- gramming language by a collection of axioms and rules of inference, which enable the proof of properties of programs, such as program correctness, in terms of speci- fied input/ output relations. The assertions about programs can be proven by either a mathematical or an operational definition and mathematical reasoning. The ax- ioms are rules of inferences that can be regarded as theorems within the framework of mathematical semantics. The objective of the axiomatic formal specification is to provide a formal system that enables a proof to be constructed using only the uninterpreted specification text. Axiomatic 5pm". and algebraic spec: Predicate specifid | ,5, pritlltjdte Sper'lllt :hat a given irnplet required {uric-tional tanstrnctiyity. Tl. iatilitates specifier and other beliayio “Jill Spat“? €llil.'lt‘r'lt dare that. given 2 its square root. \ W M Fig I4 Axiomatic specifications can be further classified into predicate specifications [15] and algebraic specifications [16]. Predicate specifications: A predicate specification explicitly describes properties of the behavior of a system that a given implementation must satisfy. The specifications describe the system’s required functionality. Predicate specifications are not bound by the constraint of constructivity. The properties can be stated separately and then combined, which facilitates specification modularity. The properties include input/output constraints and other behavior conditions, such as fault tolerance, safety, security, response time, and space efficiency. Figure 2.1 contains a predicate specification describing a proce- dure that, given an appropriate argument, 3:, computes an integer approximation to its square root. Precondition S Postcondition Precondition: :1: 2 O A integer(x); Postcondition: Vi : 0 S i g :t: : abs(x — result x result) 3 abs(x — i x i) Figure 2.1: A predicate specification of integer square root Algebraic specifications: An algebraic specification is a mathematical description language, based largely on equations, commonly used to specify abstract data types (ADT). An ADT is a well- defined data $11111” sert'it‘eS. The prop An algebraic st 0 Sort is): lllt‘ Operation. .~ syntacticallj 0 Arrow or f specifit-atittr ln Figure 233‘ given 111 the Lari: \ al ~ 1"‘3 o .1 - is. instead of d C‘éllOH IS Stirruar 15 defined data structure described by the available services and properties of these services. The properties of the data type are specified in terms of equations. An algebraic specification typically consists of o Sort{s): the names of the abstract data types being described. 0 Operati0n(s): the services applicable to instances of the abstract data type and syntactically describe how they have to be invoked (signatures). o Axioms or theorems: formally describe the semantic properties of the algebraic specification. In Figure 2.2, an algebraic specification describing the prOperties of the stack is given in the Larch specification language. Stack: 111i; introduces new: —> S push: E, S —> S p0p: S —> S asserts V s: S, e: E pop (new) :2 new p01) (push(e, 5)) == 8 Figure 2.2: A generic algebraic specification of stack 2.2.2 Operational specifications: An operational specification [17] gives one solution that satisfies the required proper- ties, instead of describing the required behaviors. Commonly, the operational specifi- cation is similar in format to a program. This approach has an advantage in that the tperatiutzal being spet'it slit-are sys tial prt‘npertf I v lUCZ'E'.’ that: a Simple in; 2.2.3 1: Th“ diff its. . 1 0r ,. 9‘ a liltmti: ”t ‘lri‘i- l H31l01 1X dffi 11)] .JTS TU): st. 16 operational specifications can be executed directly as a rapid prototype of the system being specified. Thus the specifiers and their clients can obtain feedback about the software system quickly. The disadvantages are that it is difficult to extract the essen- tial properties that the system must fulfill and the specifications tend to be relatively longer than behavioral specifications. The operational specification in Figure 2.3 gives a simple implementation algorithm to compute the square root of an integer. int sqrt (int x) reguires x 2 0; effects i=0; Whileixi abs((i- 1) x (i-1)-x) then return i - 1 else return i Figure 2.3: An operational specification of integer square root 2.2.3 Denotational specifications: The denotational specification [18] maps a specification directly to its meaning, called its denotation. The denotation is usually a mathematical value, such as a number or a function. No interpreters are used; a valuation function maps a specification directly to its meaning. A denotational definition is more abstract than an operational definition, since it does not specify computation steps. Its high-level, modular structure makes it espe- (”tally useful to lat. _ tan he studied “it; :he implement t )T t»: n. be represent .- he implemented as Therefore. dent: tion and less al at It: it tan be stated in designers. Figure 2.4 Slim cleaned by an ex: 133.35 an express'tt EXDTE‘SSlOI): 51 E31 . ‘- a set of values... C s_ to “1%: A 1) a .hereiore. 3 cm' .. f A V‘ll’TE' 0 0. 17 cially useful to language designers and users, since the individual parts of a language can be studied without having to examine the entire definition. On the other hand, the implementor of a language is left with more work. The numbers and functions must be represented as objects in a physical machine, and the valuation function must be implemented as the processor. Therefore, denotational semantics is more abstract than an operational specifica- tion and less abstract than an axiomatic specification. Like an algebraic specification, it can be stated in modules, which makes it especially useful to system analysts and designers. Figure 2.4 shows a denotational specification of boolean expressions. The value denoted by an expression depends on the state because it may contain variables. E maps an expression onto a function from states to boolean values. For a particular expression, 5, Elk]: _S_ —> _B_o<_)l is a function from _S_ to M, which corresponds to a set of values. States, S, is the set or data-type of functions from identifiers, fie, to _V_al_t;e_. A particular state, a, is a particular function from variables to values. Therefore, a specific value is obtained by evaluating the expression _E_[[e]|a: 1335;], where or gives the state in terms of identifiers and their values. Suppose o[[:t:][ = trite and 0[y] = false then the boolean expression :1: and n_ot y can be evaluated as: E122 and n_0t 31ch = E11310 A El n_0t yla = E19310 A nElz/la = lel A "Ulyl = tr_ue A nhlie = m 18 Ease: e::=a_nde| e_o_re| petsl tonal £a_1§§| 5 List 6 :2: syntax for identifiers E: Egg; —> E —> 5291 EI[€ a_n_d_ 5’]0 = E[[e]]0 /\ E]€']]0 E[[e g €']]a = E[[5]|a V E[[€']]o E[[ got 5]]0 = -: El]e]]o El] _tr_u§ ]]0 = true E[[ fag ]]a = false Elela = GM 0: Szflea Value Figure 2.4: A denotational specification of boolean expression 2.3 Specification Languages Used in Project This section overviews two specification languages that will be used in the formaliza- tion of OMT. 2.3.1 Larch The Larch family of specification languages [19] uses a two-tiered approach to formal specifications in which one tier, the Larch Shared Language (LSL), is an algebraic specification language used to specify pr0perties that are independent of a particular .A..v .‘ '1'. p‘l:.':ral.t . - ~ 5 " ;tl..t‘1l'Ll. d : . vrf. ‘1 tut. b(L‘AI‘ inlSli as used 9h, " I' LP Lll't‘lt 19 programming language and paradigm. Algebraic specifications can be used to describe object-oriented software in a straightforward manner, using abstract data types as the basic unit in software specification. Accordingly, the basic unit of specification in LSL is the trait, which axiomatizes theories about functions and data types that are used in programs. A collection of general purpose traits that are designed for constructing application-specific traits is called a trait handbook [19]. The other tier, the Larch Interface Language (LIL), specifies program behavior and programming language interfaces. For example, LCL [20] is a LIL for the C language that specifies program behavior in terms of predicate logic and function and procedure interfaces in terms of C syntax. In Figure 2.5, an algebraic specification describing the properties of the table is given in the Larch specification language. There are three operators for the table: create a new table, add an integer, and test for membership. The properties stated in the asserts section indicate that there are no elements in a newly created table and an existing element can be found using a linear search. Table: trait includes Integer introduces new: —+ Tab add: Tab, Ind, Val —+ Tab 6: Ind, Tab —+ 8001 asserts V i il: Ind, v: Val, 12: Tab '1 (i 6 new); i6add(t, i1,v) ==i=ilVi€t Figure 2.5: A Larch algebraic specification of table 2.3.2 LC LOTOS was nitgatiott 51‘1““ specification " simple extent (assists of an bra. Full LOT behayiors alur The algeli. Shared Langtt Specifit'atitms. consisting of s.- be the entire The genera parameters. w With *1“ ) org 20 2.3.2 LOTOS LOT OS was originally designed to specify the behavior of networking and commu- nication systems [21]. Basic LOTOS, based upon process algebras (an operational specification) [22, 23, 24], contains the primitives that enable specifiers to model simple external, observable behaviors without data exchange; Full LOTOS [21, 25] consists of an algebraic specification language [26], ACT ONE, and a process alge— bra. Full LOTOS enables specifiers to specify both abstract data types and external behaviors along with process communication and value passing. The algebraic specification language, ACT ONE, which is similar to the Larch Shared Language, is used to describe the abstract data types that are used in LOTOS specifications. A system, as a whole, can be specified as a single process, possibly consisting of several subprocesses. Each subprocess is considered to be a process, and thus the entire system may be viewed as a hierarchy of processes. The general form of a Full LOTOS event consists of a gate and a list of interaction parameters, where each parameter can either be a value offered at the gate (labeled with “1”) or a variable accepted at the gate (labeled with “?”). An example is as follows: 9 !3 ?data: Nat;. This event offers value 3 and accepts a value of sort Nat (natural number) for variable data at gate 9. A behavior expression models the activity of a process. Behavior expressions are built from actions and other behavior expressions by using a predefined set of operations: action prefix, choice, parallel composition, enable, and disable. for 6 his spet s at typ The rho l,lh~'.'€ kill pfOCt 2.4 4 ll LET} 115i Chjdpis he «1”. 101'; d: l ‘ . r- M p,» . t -JD-r u!) Bllliltl. pl'ilk'ldte - $39.: 21 For example, Figure 2.6 shows a typical LOTOS process algebra specification. In this specification, process statel has two gates in the form of [a,b] and a parameter s of type S. Keyword noexit specifies that the process state does not terminate. The choice operator, [], captures the notion that two alternative choices are possible. Once an event occurs, then the choice for the path to take is determined. process statel [a,b] (s: S): noexit:= b ?k:K; b !b(s,k); state1 [a,b](s) [l a ?d:D; statel [a,b](s) endproc Figure 2.6: A typical LOTOS process algebra specification 2.4 Object Model Formalization When using OMT, the object model is central to the construction of the other two models. While this dissertation focused on the formalization of the dynamic and functional models, an overview of the formalization of the object model is included for completeness sake and to provide context for the dissertation. Bourdeau and Cheng [27] identified a subset of the object model notation ap- propriate for describing requirements and added formal syntax and semantics to the notations. In object diagrams, rectangles enclose the names of classes, where a class describes a particular type of object in the system. Relationships between objects, called associations in OMT, are specified by connecting the classes involved in the relationship by models expresr turepresent at asystetn. lt n In Bonnie. instance dingy; toteryiew of I ll lot-m 22 relationship by a line with the name of the association centered on the line. Object models expressed in the context of requirements analysis are referred to as A-schemata to represent analysis object schemata. An A-schema describes the static structure of a system. It consists of a set of classes and associations among those classes. In Bourdeau and Cheng’s formalization, the semantics of the A-schemata and instance diagram notations are described by an algebraic formalization. A graphical overview of this formalization process is given in Figure 2.7. OMT semantics A—Schemata > m formalized as : testing?“ formalized as I v i v 31:31:18; ons > Algebras algebraic semantics Figure 2.7: Basic approach to formalization. In this figure, the arrow labeled “OMT semantics” represents the currently in- formal concept of consistency between an instance diagram and an A-schema. The arrow labeled “algebraic semantics” represents the formal concept of consistency be- tween an algebra and an algebraic specification that has been well-developed in the literature [28]. In Bourdeau and Cheng’s formalization, A-schemata are formalized as algebraic specifications, and instance diagrams are formalized as algebras. As a result, the OMT semantics, which were previously not well-defined, are now described in terms of an algebraic semantics. firs .11 1,, .0I _‘rjtdl‘l L' f‘J'VT '. ‘ Ll. ‘LlLAiLn BU ll aretu l ifilnynt trait isl the nun define hash: ax inthnieg and j \ 23 First, the semantics of classes, objects, and object-states will be given. Next, the semantics of associations will be addressed, and finally, the combination of all of the formalizations will be presented in order to describe the semantics of A-schemata. Bourdeau and Cheng used the Larch Shared Language (LSL) [19] to illustrate how these basic formalisms are incorporated into a structured, algebraic specification. In Figure 2.8, SPECNAME is the name of the specification module. The sorts that are to be considered as the parameters of the module are given in the parameter list following the name of the trait. Includes indicates other traits upon which the given trait is built. The introduces section itemizes function signatures, each of which gives the number and types of input arguments and result type of a function. Asserts defines the constraints for the specification. When using LSL, one assumes that a basic axiomatization of Boolean algebra is a part of every trait. This axiomatization includes the sort BOOL, the Boolean constants true and false, the connectives ‘A’ and ‘V’, implication ‘=>’, and negation ‘—.’, SPECNAME ( parameters ) : trait includes list of pre-existing specification modules to be used introduces syntax declarations for functions are listed here asserts axioms are listed here Figure 2.8: High-level structure of LSL specifications 2.4.1 1 a v 9 [‘E‘l b 011' 5. Fauna ,f. 7 .4 us a ML”. 512116 5 0' for it; put I lt‘ ‘JT cu, ICI‘ r _I *5 Hf "~_l-> 24 2.4.1 Semantics for Classes and Object States Let S be an A-schema, and let C = {C1, . . . ,Cn} be the set of class names given in S. Formally, each class name C,- E C, where 1 S i g n, is considered to be the name of a sort (type). For each class name C,, a sort Ci-STATES is introduced, which characterizes the set of states that are possible for any Ci-object. For each object- state 3 of class C,, s is specified with the signature (syntax and type specifications for input arguments and output value) 8 I —) Ci-STATES States are nullary functions with no input arguments, therefore they are considered to be constants. For every class C,, the set of possible states defined by Ci-S TA TES must include a state undefC“ in which case the state of C, is undefined. The corresponding signature is undefci : ——+ Ci-STATES' For every pair of object-states 31 and 82 of C,- (including undefci), 31 7!: 32. In order to bind a Ci-object to one of its possible states, a valuation function, $, is introduced with the signature $ : C, —> Ci-STATES , for each class name C. E C. Figure 2.9 contains a simple object model that has an object class C and its states 31 and 82 (the target of double-headed arrows). figure 2. Times 3 ‘5‘.- {:5 ru. :ng ,1 _ 25 Figure 2.10 shows its corresponding A—schema 83, containing object-states 31 and 32. Figures 2.11 and 2.12 give a summary of the formalization of the object models. Figure 2.9: A simple object model SCHEMA_diagram: trafi; includes CLASS_C CLASS_C: trait introduces err_C : -> C 82 : -> C_STATES 31 : -> C_STATES state_C : C -> C_STATES asserts fbrafl x, y: C_STATES (x=s2 / y=sl) => (X"=y); Figure 2.10: The corresponding algebraic specification of Figure 2.9 Figure 2.13 shows an object diagram of a simplified disk manager [27, 29] that is composed of (represented by a diamond) Storage and Compressor. The disk manager stores compressed data in the Storage and decompresses data that is retrieved from the Storage. We will use this example throughout this dissertation. Definitio let C be 0:. lid? 1 (0m) 1 tutti) t i0.\l3] l re: pal? [0314) l ions) 1 is a 10316) 1 3 pt ‘1 15 at they 26 Definition (Semantics of object models) : Let 0 be an object model. Let R be a binary association in 0 relating objects from classes D1 and D2. The semantics of O is an algebraic specification satisfying the following data. (0M1) Each class C in the object model 0 is denoted by a sort of the same name. (0M2) For each class C, a sort C—S TAT ES is introduced as well as two nullary functions given by undefc : —-> C—STATES , errc : ——) C . (0M3) Each object-state s, for which a double-headed arrow leads from a class C to the oval containing 3, is denoted by a function with signature 3 : —> C—STATES , and for every pair of object-states 31 and 32, the axiom 31 7E 32 is included. (0M4) For each class C, a valuation function ‘$’ is introduced with the signature 3 : C —> C-STATES The valuation of the error object is added as an axiom: $(errc) = undefc (0M5) If there is a double-headed arrow labeled a (to indicate an attribute), leading from a class C to a class D (which depicts an attribute a of C), then the function signature a:C—>D , is added to specification for class C. (0M6) If the class D in rule (0M5) is an external class, then the trait for D is included by the specification for C. If D has no parameters, then the clause includes CLASS-D is added. If D has parameters p1, . . . , pk, and there is a line connecting each p,- to a class qi, then the following clause is added: includes CLASS-p1. ..., CLASS-pk, CLASS-D ( q1 for p1, ..., Q]. for pk) Figure 2.11: Summary of Object Model Semantics tour; . (0)18] ' 3 T dr‘. 10319) 27 (0M7) Association R is denoted by the predicate R:D1,D;c —> BOOL. (0M8) The endpoints of association R determine a set of axioms. Suppose the Dl-endpoint depicts a multiplicity of m and the Dg-endpoint depicts a multiplicity of n. Then the axioms are derived by the following steps: 1. Decompose the m-to—n association R into an m-to-l and l-to—n binary association, 2. Determine the second-order specifications, P1 and P2, of each of these associations using the basis schemata, 3. Calculate the “intersection”, P, of the specifications P1 and P2, 4. Unfold and skolemize P, yielding a set of first—order axioms that are included in the trait for R. (0M9) Error object constraints are introduced: (Vd1le,d2:Dz O R(eerl,d2)/\d1;/: 87‘7‘0l => fiR(d1,d2)) , (Vd1 : D1,d2 : Dz I R(d1,err02) Adz 9‘: £1702 => fiR(d1,d2)) Figure 2.12: Summary of Object Model Semantics (continued) Disk Manager 9 t I Storage Compressor “‘3 Figure 2.13: A simplified disk manager 28 Applying the Object model formalization, Figure 2.14 contains the Larch speci- fication for the Storage Object class. Empty and non_empty are two states for the Storage class objects. The axiom in the asserts part specifies that the two states are mutually exclusive. CLASS_Storage : trait introduces orr-Storage : ->Storage empty : —> Storage_STATES non_ompty : -> Storage_STATES Stato_Storage : Storage -> Storage_STATES asserts flora" x, y : Storage_STATES (xsempty /\ y=non_empty) 8) (x ‘= y); Figure 2.14: A high-level Storage class specified in Larch Given the similarity between LSL and ACT ONE, both of which are algebraic specificationsthe previous discussion and definitions are also applicable to the ACT ONE syntax. As a means to facilitate the integration between the Object and dynamic models, we will use ACT ONE syntax instead of LSL to specify the Object model in the remainder of this dissertation. Figure 2.15 contains the ACT ONE specification for the Storage Object class. Respectively, the sorts and opns parts declare the sorts and specify the operators (constants are nullary Operators) along with the signature for the type. The eqns section lists the equational axioms that the Operators must satisfy. Empty and non_empty are two states for the Storage class Objects. The axiom in the eqns part specifies that the two states are mutually exclusive. 29 type CLASS_Storege is Boolean sorts Storage. Storage_STATES opns err_Storege : ->Storege empty : -> Storage_STATES non_empty : -> Storage_STATES Stete_Storege : Storage -> Storage-STATES eqns forall x, y : StoragejTATES ofsort Bool (x=empty /\ y=non-empty) => (x '= y); Figure 2.15: A high-level Storage class specified in ACT ONE Ch R003 Inerth Chapter 3 Related Work In this chapter, we overview related work. The related work is grouped into three categories: formalization of object-oriented development techniques, formalization of non-object-oriented approaches, and systematic refinement approaches. 3.1 Formalization of Object-Oriented Modeling Approaches This section introduces object-oriented modeling approaches. TROLL [30] and ROOA [31] propose formal semantics for the models. ROOA and the Fusion method [7] provide detailed guidelines that facilitate the derivation of models. 30 3.1.1 Overvi system is a It?! htegrai tion :34 .is 3 cc plflpen Forma Th6 pr l 3‘3 an Tsz Emilie £1 ‘ i 1. :Ji’JH-Jl _‘C‘LE‘ 31 3.1.1 TROLL—A Language for Ob ject-Oriented Specification of Information Systems Overview Jungclaus et al. developed a formal specification language, TROLL [30], to support the requirement specification phase in the early stages of object-oriented information systems development, including OMT. The underlying formal semantics of TROLL is a temporal logic [32]. Using object-oriented structuring mechanisms, TROLL integrates elements of algebraic specifications of data types [33], process specifica- tion [34, 35], the specification of reactive systems [36], and conceptual modeling [37]. As a consequence of the integration, TROLL is able to specify both the structural properties of objects via attributes and the behavior of objects through events. Formalization Approach The primary specification construct of TROLL is the class template that includes declarations for data types, attributes, and events, constraints on the observable states and on the evolution of attribute values, effects of events, behavior specification, and object activities. A class specification is composed of a class template specification and an identification mechanism that is used to distinguish individual objects of the class. TROLL also provides the abstraction mechanisms, specialization and role, to de- scribe an object from different aspects. Specialization describes objects belonging to subclasses that depend on observable properties (attributes) whereas roles describe '35: [arm C: n] TROLL. Cifilllptrll' atria-:15 l for ter; 3.2 1 mm 9 f‘“n‘-,-. fi‘.‘\!]1 32 objects belonging to subclasses that depend on certain situations during an object’s life (occurrence of events). Composite objects that are composed of other objects are also supported by TROLL. In TROLL, a composite object is specified by including specifications of component objects in the composite object specification and synchronizing the inter- actions between component objects. For a system comprising interaction objects, TROLL uses relationships and in- terfaces to define the interconnections among relatively independent objects. The relationship construct supports the specification of communication and constraints among objects. Using relationship constructs, the interconnection and communica- tion patterns among separately defined objects can be defined; the constraints among instances of classes can be described. The interface construct is used to define ob ject interfaces that are accessible to other objects, thus providing an information encapsulation mechanism. Comparison with our approach Similar to our approach, TROLL also proposes a set of formalization rules for ob ject- oriented models. Its formalization rules cover all three basic aspects of an object- oriented system (static, dynamic, and functional). The formalization is similar to ours in that objects are formalized as ADTs and dynamic behavior is specified as event sequencing patterns. However, TROLL was proposed for use in the require- ments analysis phase but not for design. TROLL has a new specification language that currently lacks tool support offered by other existing specification languages. Ill? advam constructs it to formalize derivation 0 3.1.2 R Overview list} nguri iriemed an aset of mi spaifira‘iio 8316111. Ti ration aga UnliSSitIIllS L. , R {I .iI ( l 0;in » J l-I‘H' 33 The advantage of designing a new specification language is that the structure and constructs of the language may fit the formalization objective very well. In addition to formalization rules, specific guidelines are also needed to facilitate analysts in the derivation of the formal specifications during analysis. 3.1.2 Rigorous Object-Oriented Analysis Overview The Rigorous Object-Oriented Analysis (ROOA) [38, 31, 39] formalizes object- oriented analysis notations in terms of the LOTOS specification language and includes a set of rules to conduct object-oriented analysis. The resulting formal, executable specifications of ROOA integrate the static, dynamic, and functional properties of a system. The specifications are amenable to checking the conformance of the specifi- cation against the original requirements and may be used to detect inconsistencies, omissions, and ambiguities early in the development process. Analysis process ROOA advocates a development process for object-oriented analysis. The process includes three stages: object model derivation, object model refinement, and formal specification derivation. At first, a high-level, informal object model is built by using any of the usual object-oriented analysis methods, such as the methods of Coad and Yourdon [40] and OMT [3]. During the refinement stage, the object model is completed by adding in— p [f (Isn‘t . ..tl bl di’u _. l fiche ‘, ‘. ‘ ~ .» :ghslsl delta: Form: in); Where 34 terface objects, static relationships, and attributes; the dynamic behavior is identified by defining interface scenarios, event trace diagrams (ETDs), object communication table (OCT), and adding message connections; the object model is structured into subsystems or aggregates to achieve modularity. Finally, formal specifications are derived to specify the static, dynamic, and functional properties of the system. This stage consists of the following steps: creating the object communication diagram (OCD); specifying the class templates as LOTOS processes and ADTs; composing objects; prototyping the object model by executing the LOTOS specifications; and refining the specifications according to the results of the rapid prototyping. Formalization approach ROOA formalizes objects in terms of LOTOS processes and abstract data types, where the LOTOS processes are used to specify the dynamic behavior of the objects, and the abstract data types (ADTs), given as parameters of the processes, are used to specify the state information of the objects. An object that merely plays the role of an attribute of another object is specified as a single abstract data type in ROOA. In order to avoid design issues, ROOA, proposed for use in the analysis phase, defines ADTs that contain only the necessary information to allow the specification to be prototyped with state information and values to be passed during the inter-object communication. ROOA uses a class template, which is specified as a LOTOS process definition with ADTS as parameters, to represent common features of objects of the same kind. A class that represents a collection of objects consists of a class template and an 0M id ' .l . urzqurij~ spurifia: that de Ii; ratios ‘3pr '81 68:59:; may Con 35 object identifier. An object identifier is an instance of a special LOTOS ADT used to uniquely identify objects. An Object, a member of a class, is created by instantiating a class template and is assigned a unique identification value. In ROOA, each object attribute is formalized as an ADT; each object service is formalized as an operation of an ADT. ADT operations that belong to an object specification are referenced as LOTOS value declarations in the corresponding process that describes the behavior of the object. The communication between objects are formalized in terms of LOTOS communi- cation constructs that include full synchronization, interleaving, and synchronization operators. Two objects that communicate and exchange data are specified as two pro- cesses that are synchronized through events on a gate. Complex object interactions may be built of simpler interactions by using the LOTOS composition Operators. Comparison with our approach ROOA is similar to our approach in that both use the LOTOS formal specification language to formalize the object-oriented models. However, ROOA focuses on for- mal specification derivation during the analysis phase, while we focuses on the design phase. The formalization rules of ROOA do not treat the data properties of an object as an ADT but formalize every attribute as an ADT. The approach that ROOA uses to specify the dynamic features of objects is entirely different from what we proposed. ROOA defines states as sets of attribute values and formalizes states as process pa- rameters. In contrast, we recognized that the date types and their corresponding values are not available neither during the analysis nor the high-level design stages. 3.1.1 Over Calm Dirt t merita ‘Ttriair B‘Jujrh from E 9W. t [553mm 1 .. ‘E‘wac 36 Therefore we symbolically formalized the states in terms of processes of process al- gebras and focused on the behavior in different states of an object. The functional aspect, which is another important feature of a system, is not fully addressed in ROOA. This may leave the specification incomplete for the design phase. We feel that there is too much design information included in the analysis information, such as the attributes and services provided by individual objects. This may interfere with design decisions. However, its introduction of the object identifier is interesting and may be worth investigating further. 3.1.3 The Fusion Method Overview Coleman et al. [7] proposed the Fusion object-oriented development method to sup- port the entire software development life cycle, including analysis, design, and imple- mentation. It can be used to develop sequential object-oriented systems as well as certain restricted types of concurrent systems. By integrating and extending OMT [3], Booch [41], CRC [42], and formal methods, Fusion attempts to provide a direct route from a requirements definition to a programming language implementation. How- ever, the use of formal methods in the context of Fusion does not have the typical connotation. No specific formal specification language is used to describe the models. Instead, sets of informal check lists expressed in natural language for different phases of software development are given to check the completeness and consistency of the models. -r 1 l . o J‘ .*. k l-éll; r“: ' NV 1’] 37 The approach Fusion includes a set of models and a process for software development. The graphical notations of the models are based on the existing, well-known notations, such as those of OMT [3] and Booch [41] methods. The development process divides the software life cycle into phases and indicates what should be done in each phase. Guidelines give the order of the tasks to be completed within phases and the criteria that indicate when to move to the next phase in order to ensure that development makes progress. Analysis. The analysis phase of Fusion is mainly based on OMT [3] with some variations. Unlike OMT, the individual objects during the analysis of Fusion have no interface and no dynamic behavior. Instead, Fusion focuses on the intended behavior of the system during the analysis phase. The analysis results in three models: system object model, life-cycle model, and operation model. The system object model defines the static structure of the information of a system in terms of a set of objects to be built. It is derived by eliminating the classes and relationships that belong to the environment in the original object model. The life- cycle model characterizes the allowable sequencing of system operations and events to describe how the system communicates with its environment from creation until its termination. The Operation model depicts the behavior (effect) of each system operation by defining their effect (by using preconditions and postconditions) in terms of the state change it causes and the output events it sends. The life-cycle model and the operation model together specify the behavior of a system. lbs inf l‘lillflhlt’lll‘} models [a possible 5.} l0 PllSllft'.’ ‘ other. Design. methods. defiiiitiur CRC. wl producer Object lI model. for 1 l5 deriw. in Ubjfi. Cbiilff‘lll m‘i'diél. 2 C 1 $1 « v ,. 1... (I) —. H d‘JSJr-‘P 1p"L ll] Q‘l ff] ailr" l“‘]{ 38 The informal checklist given by Fusion includes the completeness checking and consistency checking. The intent of completeness checking is to ensure that the three models (system object, life-cycle, and operation) cover all the static information, possible system scenarios, and system operations. The consistency checking is used to ensure that the information expressed by different models are consistent with each other. Design. The design phase of Fusion is based upon the CRC [42] and Booch [41] methods. During design, Fusion introduces software structures to satisfy the abstract definitions generated during analysis. The systematic design process is derived from CRC, whose main goal is to explore object interactions from the operation model produced during analysis. During design, four models are developed and refined: object interaction model, visibility model, class description model, and inheritance model. For each system Operation in the operation model, an object interaction model is derived to show how functionality is distributed across the objects of a system. An object interaction model defines the sequences of messages that occur between a collection of objects to implement a certain operation. Based on the object interaction model, a visibility model is derived for each class to describe the object communication paths in the system. A visibility model shows how a class is referenced. A class description model for a particular class collates information from the system object model, object interaction model, and visibility model to derive the methods, data attributes, and object-valued attributes of the class, respectively. Given the functional lltfilllllflll o refwrenre st derripiiuii thriiiam‘l .‘lll [ill than} 51: n the dis: Compa; fills Pip; dex'eltpr the cons the dew be used Eh. ling, infmria Sptf'ifip Pl‘l'puse Station minty 39 definition of operations in the object interaction models, the consequences to the class reference structures in the visibility models, and the class specifications in the class description models, commonalities and abstraction can be identified to introduce an inheritance model for the classes of the system. All the models produced during the design phase can be checked against the analysis models. In addition, rules are also given to check the consistencies among the design models. Comparison with our approach This approach is an attempt to integrate the best aspects of different well-known development methods. Similar to our approach, Fusion proposes checklists to check the consistency between the models in order to eliminate errors introduced during the development process. Although formal methods are mentioned and claimed to be used, there is no use of formal specification languages for representing the mod- els, thus preventing rigorous analysis of the models and leaving the checklists in an informal format. Our approach introduces formal specifications in terms of a formal specification language beginning with the analysis phase. Our development paradigm proposed for design focuses on a stepwise refinement that is based on formal speci- fications. Our approach has significant advantage over the Fusion approach in that mathematical reasoning about the properties of the target system and formal, rig- orous consistency checking between models are possible. However, the development paradigm for analysis and design of Fusion is easier to follow than that of OMT and may be useful for our design paradigm development. 3.1.4 Overvii The Ra I lllflllllf Dffl'Eff’. Lfllllf“ -. ,1 )ldlll'jg Octal. in Si, level l'nil flu; 40 3.1.4 The Unified Method Overview The Rational Corporation founded by Grady Booch and James Rumbaugh has been attempting to develop a unified method that can be used as a standard method for object-oriented software development. Joining forces with other software development methodologists (e.g., Ivar Jacobson, Bran Selic, etc.), Rational has made significant progress in the past year (1997). The promising products of Rational include the Unified Modeling Language (UML) [43, 44, 45, 46], which has been adopted as the standard object modeling language by the Object Management Group (OMG) in October 1997, the Object Constraint Language (OCL) [47] that uses simple logic for specifying invariant properties of systems comprising sets and relationships be— tween sets, and a development process, Objectory [48], that covers the entire software development life cycle. Unified Modeling Language (UML) The Unified Modeling Language (UML) is a language for specifying, visualizing, con- structing, and documenting the artifacts of software systems, as well as for business modeling and other non-software systems [44]. The primary goals of UML are as follows: 0 Provide users with a ready-to-use, expressive visual modeling language to be used to develop and exchange meaningful models. 0 Provide extensibility and specialization mechanisms to extend the core concept. 0 Be independent of particular programming languages and development pro- cesses. 0P1 difvréhr. human \Z'] 41 0 Provide a formal basis for understanding the modeling language. 0 Encourage the growth of the 00 tools market. 0 Support higher-level development concepts such as collaborations, frameworks, patterns, and components. Integrate the best software engineering development practices. UML focuses on providing ( 1) a common metamodel (which unifies semantics of different object modeling approaches), and (2) a common notation (which provides a human rendering of these semantics). The semantics of UML diagrams are described in terms of the UML metamodel. The UML metamodel is described in a combination of graphic notation, natural language, and formal language. The abstract syntax for UML diagrams is provided as a model described in a subset of UML notation, consisting of a UML class diagram and a supporting natural language description. (In this way, UML is bootstrapping itself in a manner similar to how a compiler is used to compile itself.) The well-formedness rules for UML diagrams are provided using a formal language, Object Constraint Language, and natural language (English). Finally, the semantics for UML diagrams are described primarily in natural language, but may include some additional notation, depending on the part of the model being described. In terms of the views of a model, the UML defines the following graphical dia- grams: 0 Use case diagram: describes the relationship among users and use cases (sce- narios that a system is used) within a system. 0 Class diagram: describes the types of objects in the system and the various kinds of static relationships that exist among them. 42 0 Behavior diagrams: describe different perspectives of the behavior of the objects. — Statechart diagram: shows the sequences of states that an object or an interaction goes through during its life in response to received stimuli, together with its responses and actions. — Activity diagram: is a variation of a state machine in which the states are activities representing the performance of operations and the transitions are triggered by the completion of the operations. (It represents a state machine of procedure itself; the procedure is the implementation of an Operation on the owning class.) — Interaction diagrams: describe how groups of Objects collaborate in some behavior. * Sequence diagram: shows an interaction arranged in time sequence. 4: Collaboration diagram: shows an interaction organized around the objects in the interaction and their links to each other. 0 Implementation diagrams: show aspects of implementation, including source code structure and run-time implementation structure. — Component diagram: shows the dependencies among software compo- nents, including source code components, binary code components, and executable components. — Deployment diagram: shows the configuration of run-time processing elements and the software components, processes, and objects that live on them. Object Constraint Language (OCL) OCL is a formal language that can be used to express side-effect-free constraints. UML uses OCL to specify the well-formedness rules of the UML metamodel. In the context of UML modeling, OCL can be used for a number of different purposes [47]: e To specify invariants on classes and types in the class model. 0 To specify type in invariants for Stereotypes (concrete examples). 0 To describe pre- and postconditions on Operations and Methods. 0 To describe Guard on transitions in state diagrams. e To specify constraints on operations. Bel éhilt sent ptirr Dbrra (I) 319 E a: 43 Because OCL is a pure expression language (declarative language with no side effect), the state of the system will never change because of an OCL expression, even though an OCL expression can be used to specify a state change, e.g., in a postcondition. As a typed language, OCL provides a set of predefined types, with associated operations, for modelers. The predefined types, including Boolean, Integer, Real, String, etc., are independent of any object model and part of the definition of OCL. In the context of UML, all types / classes from the UML model are types in OCL that are attached to the model. OCL expressions can refer to types, classes, interfaces, associations and data types. All attributes, association-ends, methods, and operations without side-effects (change the state of the system) that are defined on these types can be used. Objectory process Objectory [48] is a process developed by Rational to support the full life cycle of software development. Ob jectory advocates a controlled iterative process, with strong focus on architecture. It is a use-case driven, object-oriented process, using UML as a notation for its models. The Objectory process can be described in two dimensions: time and process components. In terms of time, the Objectory process divides a development cycle into four consecutive phases: 0 Inception phase: establishes the business case for the system and delimits the project scape. o ElabOration the WeCt . ConsllUCllC is ready to 0 Transition Similar 10 Oll porterrts that Ob o Requiremen velopers an supplemenll o Analysis an phase. 0 Implement; 0 Test: verift Comparison a Rational's prod quite different i: l'lll. orig: girl. :15?le our am. he notation in. er ‘7 V .mmnhuadi .llalmt‘ rnt3(],.[ a , . m object are in flat: » a flow refiner 44 e Elaboration phase: analyzes the problem domain, establishes a sound architectural foundation, develops the project plan and eliminates the highest risk elements of the project. 0 Construction phase: iteratively and incrementally develops a complete product that is ready to transition to its user community. 0 Transition phase: transitions the software to the community. Similar to other software development processes, the four engineering process com- ponents that Objectory has are: 0 Requirements capture: describes what the system should do and allows the de- velopers and the customers to agree on that description. A use-case model and supplementary requirements are the results of this component. 0 Analysis and design: shows how the system will be realized in the implementation phase. 0 Implementation: produces the sources that will result in an executable system. 0 Test: verifies the entire system. Comparison with our approach Rational’s products share a lot of similarities with our approach, yet they are still quite different in several aspects. UML originated from OMT [3], Booch’s method [49], and OOSE [50]. OMT is used in our approach as the graphical front end. The OMT notation is a subset of the notation included in UML, with the exception that data flow diagrams are not explicitly used in UML. The Activity diagram in UML shares similar concepts with our dynamic model refinement. Both of them are intended to describe how the methods of an Object are implemented. Our newly introduced SRFM that focuses on describing data flow refinement does not have a counterpart in UML. While UML notation is the tr‘irial prt; frontvetid ; lorrrral set methods 2 operators purpt‘rse. defined 1‘. l0 Slipper of OCL. and utili maphha ll is arttf Englllf‘tl lahgqa, Coilfasr l fit. L: if) 45 crucial product component from Rational, OMT notation only serves as the graphical front—end in our approach. The emphasis and focus of our approach are the underlying formal semantics. OCL in UML allows users to specify pre- and postconditions for methods and operations, and guarding conditions for state diagrams. In our approach, operators defined in the algebraic specifications (in ACT ONE) are used for the same purpose. Since OCL uses methods depicted in Class diagrams instead of Operators defined in well-defined algebraic specifications, no rewriting mechanism is available to support a rigorous reasoning of the pre- and postconditions expressed in terms of OCL. The Objectory process covers the entire life cycle of software development and utilizes UML notation. Our design process focuses on utilizing formalized OMT graphical notations to conduct a stepwise refinement during the design phase, while it is anticipated that the technique can be extended to the implementation phase of software development. In general, the underlying motivation and philosophy of Rational’s and our ap- proach are quite different. Rational attempts to introduce standardized notation for object-oriented modeling as well as a development process that utilizes the UML no- tation. A large amount of design effort of Rational’s Objectory process is contributed to demystify the design process. Concerned with the lack of familiarity of the software engineering community with formal methods, only a light-weight formal specification language, OCL, is introduced to describe a part of the system during modeling. In Contrast, the motivation of our research from the beginning has been to introduce formal methods into software development. In order to alleviate the difficulty of usulg fOrmal methods and textual, abstract formal notation, we chose OMT as the naphtha hahhirt Eilltl 59R merit of ", r. ltllllldl 3JJE OVer 46 graphical front-end and formalized its notation. A well-defined formal specification framework with sound mathematical foundation forms the basis of our formalization and serves as the back-end of the approach. Our design process is developed to utilize the formalized and integrated graphical notation in order to systematically employ formal methods during the design process. The process advocates a stepwise refine- ment of design. Because well-defined formal specifications constitute the underlying formal semantics of the graphical notation, rigorous analysis and specification analy- sis are amenable to designers. Therefore our research serves to provide a means for developers to move from an easy-to-use graphical modeling technique to the benefits of a formal description of a system amenable to automated analysis. 3.1.5 The Real-Time Object-Oriented Modeling Overview Real-Time Object-Oriented Modeling (ROOM) [51, 52] is an object-oriented method for real-time systems developed originally at Bell-Northern Research by Bran Selic and Garth Gullekson. ROOM is a method for developing real-time software that com- bines the object paradigm with advanced domain-specific modeling concepts. Special emphasis is placed on modeling the architectural levels of software that are key to re- liability, understandability, and evolvability. The method is also distinguished by its ability to take advantage of computer-based automation (through executable mod- els, reuse, and automatic code generation) for better product quality and greater Productivity. The approach ROOM includes nization irarnew The modeling time modeling 1 principle of nsin the modeling in: discontinuities i: Actors: are oh jet- models are com] along protocols described by R protocols. and ' In terms of 0 Actor cla ° ROOthl; ROOM alsl ROOM specific 47 The approach ROOM includes a modeling language, a set of modeling heuristics, and a work orga- nization framework. The modeling language. The ROOM modeling language was developed as a real- time modeling language rather than as a general-purpose language. Based upon a principle of using the same set of models for all phases of the development process, the modeling language is developed to avoid introducing any arbitrary or unnecessary discontinuities into the development process. The key concept in ROOM is an actor. Actors are objects that are independent, concurrently active logical machines. ROOM models are composed of actors that communicate with each other by sending messages along protocols. Actors may be hierarchically decomposed, and may have behaviors described by ROOMcharts, a variant of Harel’s state charts. Descriptions of actors, protocols, and behaviors can all be reused through inheritance. In terms of the views of a model, ROOM defines the following graphical diagrams: 0 Actor class diagram: captures all high-level structures of a system. 0 ROOMchart: captures the high-level behavior of actors. ROOM also has a standard ROOM linear form that can be used to represent ROOM specifications, described in terms of graphical diagrams, in textual format. This enables ROOM to subject its model specification to some type of analysis. Given the executable nature of ROOMcharts, formal analytical approaches to validation is possible. \'alitl.-. are spttifit‘d in l Modeling heu dmndmghm derelopment pr talidation and the basis for th \l'ork organi mixed with cr experience wit Opulent metht; C0Inparison ROOM and c proach attetrt 0mm pron all? different. the interactir. [Dammit for tl altar. sis. HM 51': i k to. "In; The “ v S 48 possible. Validation of ROOM models is primarily by execution of scenarios, which are specified in terms of test cases. Modeling heuristics. Based upon the modeling language, ROOM provides a set of modeling heuristics to conduct model development. The heuristics include a model development process that advocates an iterative approach to model construction and validation and heuristics that pertain to the architecture Of a system, which forms the basis for the system’s long-term evolution. Work organization. Work organization refers to the top-level process issues in- volved with creating products and managing projects. Based upon actual industrial experience with large complex projects, ROOM advocates a product-oriented devel- opment methodology. Comparison with our approach ROOM and our approach share a number of similarities. Both ROOM are our ap- proach attempt to use the same set of models for all phases of the software devel- opment process. Although the specific modeling techniques of the two approaches are different, both of them focus on modeling individual objects, their behavior, and the interaction between active, concurrent objects. The executable nature of the se- mantics for the behavior model enables both approaches to perform formal validation analysis. However, ROOM has special strength in describing static structures of a System. The key difference between the two approaches is that our approach has a well-defined, solid mathematical foundation in terms of process algebras and algebraic specificati- mtre rigrt Ralph C 3.2 This sect approarl to iorrne data hot 3.2.1 Overri. llll‘r», “‘45 {1 49 specifications, whereas ROOM relies on rigor definition of ROOMcharts. This enables more rigorous analysis methods amenable to our specifications other than validation analysis only. 3.2 N on-Ob ject-Oriented Based Approaches This section gives an overview of the formalization of three non-Object-oriented based approaches. SAZ [53] and Semmen’s method [54] both use the Z specification language to formalize structured development methods. France [55] formalized an extended data flow diagram in terms of an algebraic specification language. 3.2.1 SAZ Method Overview The SAZ Project [53] combines the benefits of the Structured Systems Analysis and Design Method (SSADM), comprising data flow and entity—relationship diagrams, with that offered by the Z specification language. In SAZ, Z can be used either as a pure quality assurance tool or as an integral systems analysis technique. Formalization approach There are two uses of Z in the SAZ project. The simpler one is its use for quality audits. A formal data model is prepared after requirements analysis and formal mOdels of logical processing are derived at the end of requirements specification in terms of Z specifications by a third party in conjunction with the development process. If any prt to he rch The process include: physica tion Oi par i ll" comp: p ([1 llll 50 If any problems or ambiguities are identified in the Z specifications, alterations have to be referred back to the development team. The other approach is to integrate the use of Z into the SSADM development process to conduct a rigorous, formal software development. The SSADM method includes five modules: feasibility, requirements analysis and specification, logical and physical design. The system state of the logical data model (LDM), which is a varia- tion of Entity-Relationship models, and parts of the functional requirements that are particularly complex or critical are then presented in the specification language Z. It comprises three main elements: the specification of the system state (or a sub-model of the state), the specification of critical processing, and the specification of selected inquiries. The specifications can also be refined with the development of the system. The principal benefits of the integrated method are: e the ability to express features of the functional system requirements that are not well documented or which have been omitted from the SSADM requirements specification; 0 the expression of all functional requirements in a common, mechanically- checkable notation; e the ability to provide (formal or informal) reasoning about, for instance, pre- conditions to operations; 0 the facility for concise expression of error processing. Compa SAZ is 2 in order logical terpart- llp'rlllli'd focuses tions. . lll hilt Sophis icate ernpl. ltgra Edéhh 3.2. 51 Comparison with our approach SAZ is also an attempt to introduce formalisms into a software development process in order to eliminate inconsistency, ambiguity, and incompleteness. The formalized Logical Data Structure (LDS, the diagrammatic part of LDM) and DF D have coun- terparts in our approach. Its formalization mechanism is entirely different from our approach. Z is a specification language based on set theory. SAZ’s specification focuses on obtaining a state specification of the system, which comprises type defini- tions, entity types, entity sets, and relationships that represent the state of a system. In addition, SAZ is currently still a proposed methodology and, so far, there is no sophisticated tool support. Our approach is based upon algebraic specification, pred- icate specification, and process algebras. We advocate an systematic approach to employ formal methods during software design process in a stepwise fashion. The in- tegration of the OMT graphical models and formal methods also makes our approach easier for the developers to use. 3.2.2 Yourdon and Z Overview For the Yourdon modeling approach, Semmens and Allen [54] have developed a Z Syntax for the Entity Relationship diagrams (ERDs), Data Flow diagrams (DFDs), and data dictionary to integrate formal methods with structured analysis. lormaliz Initially. i schema tj illlf’ft. re; are cloth schentas upon th tion sch Of erati the dia lhi Specifi- t‘art h»: lofted . - 1 their Com 52 Formalization approach Initially, Z specifications are derived from ERDs. During this stage, basic types and schema types are defined corresponding to the attributes of each entity and the en- tities, respectively; state schemas for the instances of each entity and its subtypes are derived; relationships in the diagram are declared; the entity and relationship schemas are combined to provide a complete specification of the system state. Based upon the formal specifications derived from ERDs, DFDs are formalized as Z Opera- tion schemas. The DFD does not give enough information to specify completely the operations, but some parts of the Operation schemas can be obtained directly from the diagram and the data dictionary. The result of the analysis by using the proposed integrated method is a formal specification that describes both static and dynamic properties of the system. These can help to significantly reduce the chances of specification errors remaining unde— tected until later phases of the life cycle when conventional, informal methods are used. Comparison with our approach Semmen’s approach is another attempt to formalize models of structured software development method. Its formalization of ERDs is similar to SAZ’S formalization of LDS, which is a variation of ERD. Since the dynamic behavior of the system in the Yourdon modeling approach refers to DFDs instead of state diagrams, Semmen’s approach, unlike ours, formalizes DFDs as a means to formally describe the dynamic heharior c and objec olapphca better so formalin duce fort lorrnaliz 3.2.3 OVerv france errand Contra RM 111 a applir Porn fflti: llll (Jr 53 behavior of the system. The difference that lies in the nature of structured methods and object-oriented methods puts Semmen’s and our approaches in distinct fields of application. By proposing a stepwise development framework, our approach may better serve the software development process rather than only providing a set of formalization rules. Although Semmen’s method is proposed as a means to intro— duce formalisms into analysis for structured methods, the information captured and formalized from DFDs is also applicable to our approach. 3.2.3 Semantically Extended Data Flow Diagrams Overview France defined a semantically Extended DFD (ExtDFD)[55] based on a control- extended DFD (C-DFD), which is a DFD supplemented with notation for describing control dependencies among its elements, associated with formal semantics. By giving formal semantics to the C-DFD, ExtDFD allows the specifiers to investigate desired application properties and verify semantic decompositions of data transformations. Formalization approach ExtDF D formalizes C-DFD in terms of algebraic specifications. The components of C-DFD, including the data and state transformation, asynchronous flows, external entities, and data stores, are formalized as processes; and a C-DFD is semantically interpreted as a system of communicating processes. Processes, specified algebraically by algebraic Sill and events and I The sernanti up fashion iron losing approac- l. Derive AS supphed called th 2. Derive a amongl the Sly”? DFD. is 3' Dtrive the 5y, resUltir GlVOn ll and I/O Cor Mi . 54 by algebraic state transition systems (ASTSS) [56, 57], are composed of sets of states and events and classes of behaviors. The semantics of a C-DFD are specified in terms of ASTSs generated in a bottom- up fashion from ASTSs that describe the individual C-DF D components in the fol- lowing approach: 1. Derive ASTSs characterizing the behavior of each C-DFD component from specifier- supplied descriptions. The resulting set of ASTSs, together with the C—DFD, is called the Basic Interpreted C—DFD. 2. Derive an ASTS characterizing the synchronous interactions that can take place among C-DFD components from the Basic Interpreted C-DFD. This ASTS is called the Synchronous Interaction Specification (SIS). The SIS, together with the C— DFD, is called Basic ExtDFD. 3. Derive an ASTS characterizing the permissible time-dependent relationships among the synchronous interactions specified in the SIS from the Basic ExtDFD. The resulting ASTS is called the Behavioral Specification (85). Given the formal semantics of C-DFDS in terms of ASTSs, syntactic consistency and I/O consistency are defined for the ExtDFD in order to formally and rigorously verify the consistency between levels of refinements. Comparison with our approach Although ASTS, the underlying formal specification language, is also an algebraic specification language similar to LSL and ACT ONE, the ExtDFD is significantly Int 9.. r U 55 different from our approach. The ExtDFD is proposed for structured methods; our approach is intended for object-oriented methods. The ExtDF D does not contain any model that is similar to the object model. The integration of the data flow information and control information in ExtDF D is achieved from extending the DFDs by including state and control information, whereas the integration of the two models in our approach is achieved in terms of the underlying formal semantics of the models. In ExtDFD, the formalization rules only formalize C-DFDs in terms of ASTSs but do not contribute to model integration. In our approach, the three OMT models are formalized in terms of algebraic specifications, predicate specifications, and process algebras. The integration among the models are achieved in terms of the underlying formal semantics of the models. In addition, our approach also includes a design process to take advantage of the formalization and integration techniques. 3.3 Systematic Approaches to Refinement of Anal- ysis Information for Design In this section, we describe two approaches that advocate rigorous, systematic refine- ment for software development. 3.3.1 OrerVie IBM 3 other des [liiitt‘ié to its it develop form; l'DM Seccit and (i‘ Iffifig 56 3.3.1 Vienna Development Method (VDM) Overview VDM [58, 59] was originally developed to be used for language definition and com- piler design in the 1960’s. The original objective was to develop a systematic design process that progresses from a rigorous definition of a given programming language to its implementation. Later, the objective was broadened to include the systematic development and refinement of designs. Formalization approach VDM includes both a formal description language (META-IV) and a systematic de— velopment process. The VDM design is a series of specifications in META-IV, starting with an abstract specification of the functions that the system will perform. Each specification in the series is a refinement of the previous one that is more concrete and closer to the implementation. Proof obligations that ensure the correctness of the refinement are identified and must be fulfilled by further development and refinement. The VDM [59] specification language constructs include: modules, interfaces, type definitions, state definitions, value definitions, function definitions, and operation definitions. A VDM specification defines a set of states and a set of operations that rely on and transform the states. A single Operation is specified in terms of pre— and postconditions. Given a specification, the design phase realizes data objects by data reification (refinement) in high-level design stages and develops control constructs to satisfy postconditions by Operation decomposition in low-level design stages. In addition to tilt obligations art" operation deft? Comparison VDM also lOt‘l. process. It is I The formal s; Stepwise iashi for data reifit that ensure t‘. benefit our It 57 addition to the rules that conduct data reification and operation decomposition, proof obligations are also given by VDM to guarantee the correctness of data reification and operation decomposition. Comparison with our approach VDM also focuses on stepwise design and correctness preservation in the refinement process. It is function-oriented and is suitable for structured development methods. The formal specifications are derived directly from requirements and refined in a stepwise fashion without assistance of intuitive graphical models. However, its rules for data reification and operation decomposition, particularly, the proof obligations that ensure the correctness of refinement are worthy of further investigation and may benefit our formalization of the design paradigm. 3.3.2 Correctness preserving program refinements Overview Based on Dijkstra’s work [60], Back [61] proposed a program development approach that deals with refinements concerned with data representations, control structures, program transformation rules, and implementation of procedure. In addition, the total correctness of a program can be syntactically proved (not semantically argued) by reasoning about the correctness of refinement steps in a formal system with a set of axioms and proof rules. Theapp The 11nd»; hpcl, udcmn omrfin lllfrfilllf Bar hehn langna shni lf‘llli Cm 58 The approach The underlying logic that carries out proofs of program properties is an infinitary logic, Law, which is an extension of ordinary first-order logic, that allows disjunctions and conjunctions over a countably infinite number of formulas and quantifications only over finite sequences of variables. There are also inference rules that have a countably infinite number of premises. Back used the language of descriptions to describe state transformations, that is, the language is used to specify a program. The primitive statement constructs of the language includes: a nondeterministic assignment, control structures of composition, selection, iteration, and nondeterministic binary choice. Having a set of theorems for proving refinement correctness in terms of weakest preconditions, Back further proposed a top-down stepwise refinement using descrip- tions. The proposed formal development approach allows the use of proof rules for refinement to establish the correctness of the refinement steps. Comparison with our approach Both Back’s and our approaches advocate a stepwise refinement during the software development process. However, Back’s approach deals with the refinement of low- level program development and algorithm design, whereas ours focuses on high-level specification refinement during the design process. The application areas of Back’s method and ours are totally different. Back’s approach mainly treats the develop- ment of procedures and assumes that the Specification of program termination can be mount rhea 10 llit‘ hnhe acquired and directly represented in terms of wa. Our specification derivation may serve as the preceding stage for Back’s method. This method is directly applicable to the implementation of the detail design specification and may be valuable for our further research when we move from design to the implementation phase. Chapter 4 Object Model Formalization Revisited In this chapter, we re-examine the object model formalization and introduce a new formalization rule for the object model. 4.1 The Derivation of Algebraic Specifications Although the algebraic specification shown in Figure 2.15 can be used for requirements analysis purposes, it does not provide sufficient design information for implementation such as attributes and operations. The original intent of the object diagram formal- ization [27] was to define formal semantics for the high-level object diagram used in the analysis phase, where these specifications should be amenable to refinement to include design details. However, the acquisition of such detailed specifications is not easy to obtain and requires more information than can be directly determined from 60 S‘i'Sl t? erati iOl 61 the formalized object diagrams. Since the design stage typically introduces more de- tails about operations that describe the system behavior, we use information from the functional and dynamic models to contribute to the design specifications. The functional model represents the operations and data transformations of the system in terms of data flow diagrams. At the most detailed level, each of the op- erations, or processes, are operators of objects depicted in the object model. The process bubbles in a data flow diagram determine the services of the system, thereby defining the operators for the objects and the events, actions, and activities in the dynamic model. From the formalization perspective (see Chapter 6), the signature of a given operator for an object is determined by the input and the output data flows to/ from the corresponding process bubble. This signature information is used in both the object model definition during the design stage and in the dynamic model specification. 4.2 Distinguished Sort In a specific problem domain, by sharing some commonality, a set of objects can be abstracted into a class. In the world of software engineering, the commonality is represented as attributes that are expressed in terms of specific data values. In the corresponding algebraic specification for a class of objects, each attribute is repre- sented by a data sort that denotes a range of values for the attribute. In order to refer to the set of sorts for attributes of an object class, a sort that represents the object class and a tuple operator can be introduced into the algebraic specification. The sort the tip - ttrihnt SUI I IO,l struct ' of an t its att rigors ft. Ll" ,. .14- VT 62 The sort of the Object class is defined as distinguished sort, which is sometimes called the type of interest or data sort [19]. The tuple operator is proposed to contain the attributes of an object to form a value of the distinguished sort. The distinguished sort together with the tuple operator are like a typical record type declaration con- struct provided by most programming languages. If, for some reason, the attributes of an object class cannot be identified, an abstract sort can be declared as the dis- tinguished sort instead. The abstract distinguished sort may be refined into sorts of its attributes later during the design process when it is necessary. In order to achieve rigorous specification, we insist that every object class must have a distinguished sort. For instance, every person in our society has a gender and a social security number (SSN). In the world of computer science, this commonality is represented as attributes for the person class. In terms of algebraic specifications, the Person distinguished sort with Gender and SSN as attributes results in the LOTOS specification in Figure 4.1. In this specification, the tuple operator is also named Person. 4.3 An added formalization rule In addition to the object model formalization rules given in Section 2.4, another rule, OM10, is added to formalize the attributes of an Object class in terms of a distinguished sort. The attributes of an object are a list of variable-type pairs in OMT’s object model. The motivation for this rule is to enable access to individual attribute values. The object class and types of attributes are formalized as sorts of algebraic specifications. A tuple that maps from the sorts of attributes to the sort 0i the? II] ter l“trial 63 type Person is sorts Person, Gender, Nat opns male : —> Gender female : -> Gender Person : Gender, Nat -> Person getgender : Person -> Gender getssn : Person -> Nat eqns forall p: Person, 5: Nat, g: Gender ofsort Person Person (getgender(p), getssn(p)) = p ofsort Gender getgender(Person(g,s)) = g ofsort Nat getssn(Person(g,s)) = s endtype Figure 4.1: The ACT ONE specification for person of their corresponding object class is also introduced. The variables are formalized in terms of operations that map from the sort of the object class to the sorts of the variables. lllrgtj Title I 64 OM10 The attributes, in the form of variable-type pairs, of an object class are formalized as sorts and a tuple that maps attribute types to the distinguished sort that represents the object class. For Object 0, given attributes a1 : A1,a2 : A2,...,an : An (where a1,a2,...,an are variables and A1,A2, ...,An are types), create the following expression in LOTOS specification typedef 0 is sorts C), 14-1, i4-2, . .., zl-n opns 0 : A-1, A_2, ..., A-n ——> 0 get_a-1 : 0 ——) A_l get_a_2 : O —-) A_2 get an : O —) A-n eqns forall a_1: A-1, a_2: A_2, ..., a_n: A.n ofsort.A_1 get_a_1(0(a_1, a_2, ..., a_n)) = a_1 ofsort A_2 get_a_2(0(a_1, a_2, ..., a-n)) ofsort A_n get_a.n(0(a-1, a_2, ..., a_n)) (1.2 II .9 :3 endtype Regardless of whether attributes are given to object 0, sort 0 is treated as the dis- tinguished sort. Figure 4.2 gives a sample object diagram. Based upon formalization rule OM10, the automatically generated formal specification is shown in Figure 4.3. d1: D1 d2: D2 d3: D3 Figure 4.2: A sample object model that contains attributes for object O typedef sor op: Mi 3 SEI 0 o ’: ‘7‘ « , 357k If.I J1 to II".- “AME lye" Illa' II wa 65 typedef 0 is sorts 0, D1, D2, D3 opns 0 : D1, D2, D3 -> 0 get_d1 : 0 -> Di get_d2 : 0 -> D2 get_d3 : 0 -> D3 eqns forall d1: 01, d2: D2, d3: D3 ofsort Dl get_d1 (0(d1, d2, d3)) = d1; ofsort D2 get_d2 (0(d1, d2, d3)) = d2; ofsort D3 get_d3 (0(d1, d2, d3)) = d3; endtype Figure 4.3: The automatically generated formal specification from the sample object model 4.4 Formal Representation of Algebraic Specifica- tion An algebraic specification can be represented as a tuple (<1), 1", \II, gt), where is a set of sorts, P is a set of operators with their signatures, \11 is a set of axioms, and (b (E (1)) is a distinguished sort. The operators I‘ can be classified into four categories: generators, observers, extensions, and auxiliaries. The generators create all the values of the distinguished sort. The extensions are the remaining operators, such as delete, whose range is the distinguished sort. The observers are the operators whose domain includes the distinguished sort and whose range is some other sort. The auxiliaries are similar to observers but the domain does not include the distinguished sort. _——_.._.__ _ __ 66 In order to facilitate the discussion of the dynamic model formalization, we orthog- onally classify the operators as modifiers and non-modifiers. The modifiers include generators and extensions, whose range is the distinguished sort; the non-modifiers consist of observers and auxiliaries, whose range is some other sort. Thus I‘ is parti- tioned into two mutually exclusive sets, 9 and O, where Q is the set of modifiers and O is the set of non-modifiers. According to this classification, operator 0 in Figure 4.3 is a modifier; operators get_d1, get_d2, and get_d3 are non-modifiers. Ch 1’. AU ll} [’3 liar Ld. Chapter 5 Dynamic Model Formalization The dynamic model in OMT [3] is based on David Harel’s statecharts [8]. In our formalization [62, 63], we retain the hierarchical structure and most of the syntactic notations of statecharts. The OMT approach for creating state diagrams is to create numerous scenarios, generate event trace and event flow diagrams from the scenarios, and then create state diagrams from the event diagrams. Although this ad hoc ap- proach may be useful in determining necessary operations of objects and interactions between objects, the lack of explicit formal semantics makes the derived dynamic models inherently exempt from formal, automated analysis. Therefore we define a formal semantics for the dynamic model so that formal specifications can be derived for the reasoning and analysis at the intra—model and inter-model levels. We have chosen LOTOS as the formal specification language to describe the dy- namic models of OMT. The major motivations for selecting LOTOS as the target specification language are as follows. 67 68 o It has a sound mathematical foundation defined in terms of process algebras and algebraic specifications so that formal analysis can be conducted. 0 It provides support for integrating algebraic specifications with process algebras. o It supports concurrency. 0 There are numerous support and analysis tools. 0 The behavior specifications are executable thus enabling behavior simulation and requirements validation. o It has been accepted as an ISO standard and has been successfully used for numerous industrial projects [64, 65, 66]. The remainder of this chapter is organized as follows. Section 5.1 discusses a preliminary formalization of the state diagrams. Section 5.2 gives the formalization of the dynamic models for individual objects. Section 5.3 shows how concurrent state diagrams are formalized. Section 5.4 discusses the integration of the dynamic model with two other models. Section 5.5 summaries the chapter. 5.1 Preliminary Formalization In OMT, a state diagram is used to describe the aspects of a system that are concerned with time and change, flow of control, interactions, and sequencing of operations in a system of concurrently active objects. In general, this objective is ambitious. Accordingly, we restrict the dynamic model to describe only the (observable) behavior of a system. (Unless otherwise noted, behavior refers to observable behavior.) Observable behavior. The observable behavior of an object, as the name implies, refers to its interactions with the environment and the sequences of interactions that 69 can take place. The interactions can be observed outside of the object; the environ- ment can either be other objects or the system environment. Definition-1: Observable Behavior: Observable behavior is defined to be in- teractions (inter-object communication and object operations) between the object and its environment and the interaction pattern. Dynamic model. In most cases, interaction is a synonym for communication. Here, the interaction includes the inter-object communication and the action ini- tiation and reaction of the objects. The inter-object communication is the communi- cation between objects. Therefore, the behavior of an object consists of all its possible communication and operation sequences with the environment. Definition-2: Dynamic Model: The dynamic model formally specifies all the possible interaction patterns of an object; inter-object communication and object op- erations are considered interactions. Communication model. The communication mechanism is not explicitly ad- dressed in OMT [3]. The state diagrams in the text imply a broadcasting communi- cation mechanism. Figure 5.1 shows a typical Harel statechart (with a broadcasting communication mechanism [67]), whose notation is used in OMT and other process- control modeling systems, including RSML [68]. The condition, in( G), under which event f triggers the state transition from B to C is valid in statechart notation. How- ever, when the statechart is introduced into an Object-oriented methodology without any modification, potential problems arise. Since A and D are two concurrent states, 70 they are actually the dynamic models of two independent objects in OMT. Because the class objects are encapsulated information, information is passed only by meth- ods, the only inter-object communication mechanism. Obviously, condition “D is in G” is not visible to A, and therefore it is invalid to use dynamic models of OMT in exactly the same way as the original statechart is used [67]. fl-—-—-—-——_q Figure 5.1: A typical statechart With respect to information encapsulation, one key characteristic of any object- oriented methodology is that a change in an object is not visible to external objects. The only means that a change can be reflected to other objects is through inter-object communication. Accordingly, the inter-Object communication is the only communi- cation mechanism in the formalized model; the visible events of an object are carried by the inter-object communication external to the object. Definition-3: Communication Model: Inter—object communication is the only communication mechanism in the formal model. 71 5.2 Formalizingstate diagrams of individual ob- jects In this section, we briefly introduce the formalization of the dynamic model in terms of a LOTOS specification. In order to facilitate our discussion and the presentation of the formalization, a state diagram is represented as a tuple D = (S, 23 A) A, (p) C1 Ea ill, A) 6) {pa C) 80) CO), “There S is a finite set of states; so is the initial state in D E is a finite set of events A is a set of variables A is a set of actions and activities, and A g I‘ (P are operators defined in the corresponding algebraic specifications derived from object and functional models) (I) is a set of data sorts defined in the corresponding algebraic specification C is a set of guarding conditions; c0 represents an empty condition that always holds (true) 5 is a set of external events to be triggered if) : S x )3 X C t—> S; tb is a transition function mapping S x E x C to S (1,!) can be a partial function) A : S l—> A; A is a function that associates a state with an activity (A can be a partial function) 6 : S x E x C t——> A; 6 is a function that associates a transition with an action (,0 : S x E t—> 2"”; cp is a function that maps a state and an event to a set of variable-data-sort pairs that are associated with the event C : S x E x C +—+ E; C is a function that maps a transition to an external event to trigger In the process of bringing formalisms into the dynamic model, we introduced some new notations in order to enhance the formality of the state diagrams (The lli’Oél simil 72 most recent release of UML [69, 70] indicates that its state diagram is also using a similar set of notations.) Figure 5.2 gives a typical state diagram with an initial state and three state transitions. A label on an arc in the format of e(d1 : D1,d2 : D2,...,d,, : Dn)[c]/a(dx1,dm2,...,dxm)"0.e’(dy,,dy2,...,dm) denotes an event 6, data items (d1, d2, ..., dn) associated with the event e, a guarding condition c, the corresponding action a, and the event 6’ of object O to be triggered. The remainder of this section introduces formalization rules for each component of a state diagram. The application of these formalization rules yields a portion of the formal specification of the corresponding state diagram. el(d11:Dll,d12:DlZ ..... d1m:Dlm)[cl] /al(d12,dlm)"01.e2(dl l,d13) eZ(d21:D21,d22:D22 ..... d2n:D2n)[c2]/a2 e3/a2"02.el Figure 5.2: A typical state diagram 5.2.1 State The derivation and justification of object states is one of the most difficult issues for dynamic modeling. The root of this difficulty is that the role of the states is not clearly defined within OMT. With the formal definition of the dynamic model given 73 in Definition-2, it is straightforward to ascertain that the basic function of the states is to describe the different interaction sequences. Since the formalized object model requires that every leaf class contain a distin- guished sort (type of interest), we model the behavior of a leaf class as an individual state diagram, whose states are determined by partitioning the values of the distin- guished sort into classes. DFR-l The object states S are formalized as LOTOS processes. For every state 3, s E S, create the following LOTOS expression process 5 : noexit := endproc Given that most transitions involve attribute value changes, the processes that formally specify the states are associated with a parameter of the distinguished sort. DFR—2 Every process that formally specifies a state 3 is associated with a parameter :r of the distinguished sort 4). For every state 3, s E S, and distinguished sort 45 E , create the following LOTOS expression process 5 (x: (p): noexit z: endproc 5.2.2 Communication model and event An event is defined as inter-process communication because only the observable ex- ternal behavior is well-defined and thus can be modeled. While this convention may seem restrictive, it is well-defined and exactly models the communication in the real world; it also achieves information encapsulation in the event definition. fora gin observable lit Therefore. tl: The gate world and is events of thr corrrrnunicati that correspt x DFR‘3 The eve commun event5,j E L. E] For ever or. Q] pri en \ for those fOlmalize the \ on Its type (it 74 For a given object, the use of an operator determines whether it corresponds to observable behavior (that is, inter-object communication) or is internal to the object. Therefore, the inter-object communication is a subset of the object Operators, F. The gate construct in LOTOS is used to describe the interface to the external world and is able to accept and deliver data. It is straightforward to specify the events of the dynamic model as gates in LOTOS specifications. The inter-Object communication (message passing) is modeled as an event arriving at a certain gate that corresponds to a specific operator. DFR-3 The events of an object together with the events to be triggered are formalized as the inter-object communication external to the object, which is a subset of I‘ (set of the object Operators). The events, 2, and events to be triggered, E, in a state diagram D are specified as a formal gate list [2 U E] for the processes in S. For every state 3, s E S, distinguished sort (p, events 2, and events to be triggered E (d) E , E Q P), create the following expression process 5 [E U E](x: (t): noexit 2: endproc For those events that are associated with arguments, the following rule is used to formalize the event definition.1 1The notations x,- : a,- and (x,,a,-) are used interchangeably, both of which represent a variable and its type declaration. Dill-4 ‘ In objec‘ the cc ‘\ I)FIt-5 is Cc Si iii. 3:1} D (7:, \ 75 DFR—4 Attribute pairs 9:,- : a,- (data items) associated with an event e are formalized as variable decla- rations ?x,~ : 0,- associated with a LOTOS gate e. For every state 3 and event 6 (s E S,e 6 E), distinguished sort 4), events 2, and events to be triggered E (d) 6 Q,E (_Z I‘), if the partial function cp maps (s,e) to pairs x1 : a1,x2 : a2,...,x,, :an, a non-empty subset of A x Q ({(x1,a1), (x2,a2), ..., (xn,an)} E 2"”), create the following expression process 5 [E U E](x: a): noexit := e ?x1:a1, ?$2 202, ..., III?” :a,,; endproc If the partial function go maps (s,e) to an empty set (no associated attribute for event e), create the following expression process 5 [E U E](x: (b): noexit :2 9: endproc In some cases, a transition may be associated with a triggerable event of another Object. This case is formalized as a value declaration of the data to be transferred at the corresponding gate. DFR—5 An event to be triggered, e’, is formalized as a value declaration (Iy,) at a LOTOS gate. For every state 3, event 6, and condition c (s E S,e E E, c E C), distinguished sort (,3, events 2, and events to be triggered E. (o 6 Q, E _C_ I‘), if the partial function 6 maps (s,e,c) to a triggerable event e’, create the following expression process 5 [E U E](x: rt): noexit z: e’ lyl, lyg, ..., lym; endproc, where {y1, y2, ..., ym}, a subset of {3:1, 1:2, ..., 2:”, x}, is specified in the corresponding state diagrams. 5.2.3 Condition A condition, in the form of predicates, is used to describe circumstances under which a state transition can take place. We formalize guarding conditions as LOTOS guarded expressions in form of a predicate preceding a behavior expression, which becomes possible when the predicate holds. —_— DfR-G Aguard For ever 5:. and c 01.1") I a non-ow procei e ? endpr where I A predica of an Optj'rat' \- DFR-7 A new] Boolean Given a 50” 0. sons .\' Spec type: 0F endt proc end; ends \ 5.2.4 A The activiti. abehal’ior s 'i {11%pr all? Sp< aSr \~. Jperdtor 76 DFR—6 A guarding condition c is formalized as a guarded expression [c]. For every state 3, event 6, and condition c (s E S, e E E, c E C), distinguished sort 4), events 2, and events to trigger E ((15 E (I), 2 C_: I‘), if the partial function (p maps (s,e) to pairs 2:1 : 01,32 : a2,...,:1:,, : an, a non-empty subset ofA x ({(zrl,a1), (x2,a2), ..., (:rn,an)} 6 2A“) a non-empty subset of sorts ({al , a2, ..., an} E 24’), and c aé c0, create the following expression process 5 [2 U E](x: (1)): noexit := e ?$1 101, ?$2 I (12, ..., ?.’13n : (In; ([C] —) ...) endproc, where 31,32, ..., 3:” are variables to hold the attributes associated with the event. A predicate that is newly introduced in a guarding condition is formalized in terms of an operation of Boolean sort in the algebraic specification section. DFR—7 A newly introduced predicate in a guarding condition is formalized as an operation of type Boolean in the algebraic specification section. Given object D, for every state 3, event 6, condition c (s E S, e E 2, c E C), distinguished sort 43, and predicate p introduced in condition c, if 331,32, ...,mn are the arguments for p of sorts X1, X2, ..., X", create the following expression specification D [2 U E](x: 45): noexit typedef 43 is Boolean opns p: X1,X2,...,X,, —> Bool endtype process 5 [2 U E](x: d): noexit := end proc endspec 5.2.4 Action and activity The activities and actions are defined as operators in the algebraic specification (ac- tions are considered instantaneous; activities may occur over a period of time). Since a behavior specification in LOTOS can reference the operators that are defined in the algebraic specification part, we model the actions and activities in the state diagrams as operator references in the LOTOS specification. The difference between activities {labeled grag termine. it i should be m An actiaz operator (de DFR-8 An ac COHESD' For err maps t C # C0. expires pro “Or F0: an. In; 77 (labeled graphically as “do: activity”) and actions is not straightforward to de- termine. It depends on the experience of the designer to determine which operators should be modeled as activities and which operators should be modeled as actions. An action can be formalized in terms of a value declaration by a reference to an operator (defined in the algebraic specification) at the corresponding gate. DFR—S An action a is formalized in terms of a value declaration la by an Operator reference at the corresponding gate e. For every state 3, event e, and condition c (s E S, e E Z, c E C), if the partial function (,0 maps tuple (s,e) to sorts a1,a2, ..., an (a non-empty subset of sorts (I) ({a1,a2, ...,an} 6 2°», 0 ¢ co, and the partial function 6 maps tuple (s, e) to an action a (a E A), create the following expression process 5 [E U E](x: o): noexit := e 72:1 :al, ?:1:2 :az, ?:r,, : an; (M -+ e !a(y1. y2. ym)) endproc, where {y1, y2, ..., ym}, a subset of {2:1, 2:2, ..., at", x}, is specified in the corresponding state diagrams. With the built-in internal event, 2', predefined in LOTOS, we are able to specify the activities as value declarations preceded by an internal event, which can be interpreted as “the return of a result takes time to complete.” DFR-9 An activity a is formalized as a value declaration la at the corresponding gate 6 preceded by a nondeterministic internal event 2'. For every 3, 3 E S, distinguished sort qfi, events 2, events to be triggered E (d) E (D, 2 Q I‘), and arguements y1, y2, ..., yn of sorts Y1, Y2, ..., Yn for activity a, if the partial function /\ maps state 3 to an activity a (a E A), create the following expression process 5 [E UE](x: 43, y; :Yl, y; : Y2, yn : Yn): noexit := i; e !a(y1. yz. yn); endproc Consider the state diagram of the Compressor object shown in Figure 5.3. As a notation convention in the discussion of diagrams and specifications for diagrams, the italic font will be used to denote diagram components and the courier font will denote: tion in the rim ('L‘rmpltj as acti done E the to result: y’h 78 denotes specification components. The compress and decompress operations transi- tion from state idle to compression and then to decompression, respectively. Since the compress and decompress operations, which may take some duration of time to complete, cannot be considered instantaneous, they should no longer be modeled as actions, but, instead, considered as activities in the corresponding states. The done event, (denoted by an unlabeled arrow leaving an activity state), representing the completion of compression or decompression, activates the actions to return the results and trigger state transitions. [ Compressor: c / W decompress(d:D) compress(d:D) W compression decompress(d) compress(d) \ j Figure 5.3: The state diagram for the Compressor object Figure 5.4 contains a complete LOTOS specification for the Compressor class based on the formalization rules presented thus far (the exception is that the con- struction of specifications for transitions which is discussed next). The specification describes both the abstract data type and the behavior of a Compressor object. The first part of the specification describes the abstract data type of the object class in terms of ACT ONE; the second part captures the object behavior in terms of pro- cess algebras. The expression “i;cornpresslcompress(data)” exactly models the compress activity in the state diagram. The behavior specificatoin captures: ol F!) 5.2. The Obj. 6.. aim 79 o The Compressor is initially in idle state. a A decompress request triggers the transition from idle state to decompression state. a In the ldecompression! state, the Compressor performs the decompression activity. 0 Upon the completion of the decompression activity, the Compressor returns the decompresed data and transitions back to idle state. 0 A compress request triggers the transition from idle state to compression state. 0 In the lcompressionl state, the Compressor performs the compression activity. 0 Upon the completion of the compression activity, the Compressor returns the compresed data and transitions back to idle state. 5.2.5 Transitions The change of state caused by an event is a transition. Although an event, inter- object communication, or internal event, is the cause of a transition, the transition is actually triggered by the corresponding action or activity. However, a state transition does not necessarily imply a state change. Only those transitions whose starting state is different from its ending state can cause a state change. Since only modifier operators can trigger a state change, the state transition that is fired by a non-modifier does not change state. DFR—lO A transition can cause a state change if and only if the action that corresponds to a transition is defined as a modifier Operator. For every state 3 and event 6 (s 6 S,e E E), if the partial function 1p does not map tuple (s,e) to state 3 (3 ¢ ¢(s,e)), then the partial function 6 maps tuple (s,e) to a modifier operator (6(s,e) E 0); if the partial function 6 maps tuple (s,e) to a non-modifier operator (6(s,e) E 9), then the partial function 11) maps tuple (s,e) to state 3 (s = w(s,e)). specifi library Nat endlib type ( sort Co: opn- um co: de: 5 i: eqn; fc endty helm Idle wher: pro Em PM 9111 Ends1 80 specification Compressor [compress, decompress] (c: Compressor): noexit fibmary NaturalNumber endlib type Compression is NaturalNumber sorts Compressor, Data (urns undef_data : -> Data compress : Data -> Data decompress : Data -> Data sizeof : Data -> Nat eqnw forall 1:: Data ofsort Nat sizeof(undef_data) = O; ofsort Bool sizeof(x) = 0 => x = undef_data; sizeof(x) ge sizeof(compress(x)) = true; sizeof(x) 1e sizeof(decompress(x)) = true; ofsort Data decompress(compress(x)) = x; endtype behavior Idle_State [compress, decompress] (c) where process Idle_State[compress,decompress]: (c: Compressor) noexit:= compress ?data:Data; Compress_State[compress,decompress] (c, data) [I decompress ?data:Data; Decompress_State[compress,decompress] (c, data) endproc process Compress_State [compress,decompress] (c:Compressor,data:Data): noexit:= i; compress !compress(data); Idle_State[compress,decompress] (c) endproc process Decompress_State[compress,decompress](c:Compressor,data:Data)::noexitu: i; decompress !decompress(data); Idle_State[compress,decompress] (c) endproc endspec Figure 5.4: A Compressor class and its behavior specified in LOTOS 81 The state transitions in the dynamic model of OMT are formalized in terms of LOTOS process instantiations. DFR—ll The state transitions are formalized as process instantiations. For every state 3 and event e (s E S, e E Z), distinguished sort at, events 23, and events to be triggered E (d) E Q, 2 Q P), if the partial function 90 maps (3, e) to pairs 2:1 : a1,a:2 : a2, ...,:rn : an, a non-empty subset of A x Q ({(x1,a1),(:rz,a2),..., (zn,a,,)} 6 2““), the partial function 6 maps tuple (s, e) to an action a (a E A), the partial function d) maps tuple (s, e) to a. state 3’ (s’ e S), and a is of sort ()5, create the following expression process 5 [2 U E](x: d): noexit z: e ?2:1 :01 ?:2:2 :a2 ?:r,, : an; S’lE U Shah/1.312. yml) endproc if a is not of sort q), create the following expression process 5 [E U E](x: d): noexit 2: e ?2:1:a1?:r2:a2 711:" :an; e !a(y1, y2, ym);s’[EUE](x) endproc In cases, where there are multiple state transitions from a single state, the multi- ple transitions are specified as multiple process instantiations composed by a choice operator (“[1”). DFR-12 Multiple state transitions from a single state are formalized as process instantiations composed by a choice Operator (adding more transitions may add more choice Operators. For every state 3, events e1 and e2 (3 E S, 61,82 6 2), distinguished sort ()3, events 2, and events to be triggered E (d E Q, 2 g P), if e1 79 eg, the partial function (p maps tuple (s,el) to {$11 2 011,112 I (112,...,$1n I {11"}, (3,82) 130 {$21 I (121,1722 2 (122,...,$2j I a2j} (where {($11,011).)$12,012),---,($1main)},{($21,021),($22,022),---,($2j,02j)} E 2Ax¢ly the partial function 6 maps tuple (3, e1) to al, (8,62) to a2 (a1,a2 6 A), and the partial function 1,!) maps tuple (3, cl) to 31:, (3, eg) to 32:, create the following expression‘ process 5 [2 U E](x: d): noexit := e1 ?:1:11 :a11 11:12 : 012 ?:r1,,:a1,,; 6: lai(yn 1112 yim): silleEMX) 82 ?.’€21 $021 ?$22 I (122 ?£E2J‘ 1021'; 62 !32(y21 3122 312k); 5242 UEKX) endproc ‘The expression may differ according to DFR—lO depending on the sort of a,. 5.2.6 Given ferrna DFR-l.‘ 82 5.2.6 State diagram Given the formalization rules for the components of a state diagram, we are able to formalize the diagram in terms of its components. DFR—13 A state diagram can be formalized as either a LOTOS specification or a LOTOS process definition. For state diagram D = (S, 2, A,A, Q, C,E, 1,1), A, 6, «,9, C, so, c0), we can have either process D [2 U E] (x: a) :noexit := $0 [3 U E] (X) where ( algebraic specification ) ( process definitions ) endspec OR specification D [2 U E] (x: a) :noexit ( algebraic specification ) behaviour 50 [>3 U 5] (X) where ( process definitions ) endspec, where the first format is used if the process will be composed within other specifications to form more complex behavior specifications; the second format is used if the specification is a top level specification. An example. Figure 5.5 gives a dynamic model for Storage that corresponds to a part of the object diagram given in Figure 2.13. Its corresponding class and behavior specifications are given in Figures 5.6 and 5.7. In Figure 5.5, the empty and non_empty states are formalized as the empty_state and non_empty_state processes, respectively in Figures 5.6 and 5.7. The events, insert, retrieve, and delete, are formalized as the three gates visible to the external objects. The guarding conditions are “count(s) gt Succ(0)” and “count(s) eq Succ(0)”. Since empty_state is the default state that a Storage object enters when it is initially created, the behavior of a Storage object is specified I I Speci librar Boc endli 80! Up; 9Q 9116 83 l Storage:s l inscrt(d:D,k:K)/insert(s,d,k) insert(d:D,k:K)/insert(s,d,k) U retrievc(k:K)/retrieve(s,k) delete(k:K)[count=l ]/delcte(s.k) delete(k:l()[count>l ]/dclete(s,k) L / Figure 5.5: The state diagram for Storage specification Storagefinsert,retrieve,delete] (3: Storage): noexit fibrary Boolean, NaturalNumber endlib sorts Storage, Data, Key opns new : -> Storage undef_Data: -> Data undef_Key : -> Key count : Storage -> Nat retrieve : Storage, Data, Key -> Data delete : Storage, Key -> Storage - eq _ : Data, Data -> 8001 _ eq _ : Key, Key -> 8001 eqns flora“ d: Data, k, k1, k2: Key, 3: Storage ofsort Nat count(new) = O; count(insert(s,d,k)) = Succ(0) + count(s); ofsort Data retrieveP(new,d,k) = undef_Data; (k1 eq k2) => retrieve (insert(s,d,k2),k1)= d; not(k1 eq k2) => retrieve (insert(s,d,k2),k1) = retrieve (3, k1); ofsort Storage delete(new,k) = new; (k1 eq k2) => delete(insert(s,d,k2),k1)=s; not(k1 eq k2) => delete(insert(s,d,k2),k1)= insert(de1ete(s,k1),d,k2); endtype Figure 5.6: The specification (in Full LOTOS) of the Storage (1) enu pn ends Shin 93p: PTOQ all {3' U151 84 behavior empty_state[insert,retrieve,delete] (s) where ‘process empty_state[insert,retrieve,delete](s: Storage): noexit:= insert? d : Data ? k : Key; non-empty_state[insert,retrieve,delete](insert(s,d,k)) endproc process non_empty_state[insert,retrieve,delete](s: Storage): noexit:= retrieve ?k:Key; retrieve !retrieve(s,k); non_empty_state[insert,retrieve,delete](s) [I insert ?dzData ?k:Key; non_empty_stateEinsert,retrieve,delete](insert(s,d,k)) i] delete ?k:Key; ( [count(s) gt Succ(0)] -> non_empty_state[insert,retrieve,delete](delete(s,k)) [l [count(s) eq Succ(0)] -> empty_state[insert,retrieve,delete](delete(s,k)) ) endproc endspec Figure 5.7: The specification (in Full LOTOS) of the Storage (2) as “empty_state[insert,retrieve,de1ete](new).” This specification enables a Storage object to enter the empty state when it is first initialized. The transition from empty to non_empty triggered by the insert event is formalized in the empty_state process as: insert?d : D?k : K ; non_empty_state [insert , retrieve , delete] (insert (3 , d , k) ). The specification “insert ?d:D ?k:K;” indicates that the process is to wait for an event to occur at the insert gate. In addition, two data values of type D and K must also be associated with the upcoming event at gate insert. the: DOD H011 3p; 85 Once an insert event with the two required data values occurs at the insert gate, the insert action is performed and the transition from the empty state to the non_empty state is triggered. The transition is formalized as the process instantiation non_empty_stateEinsert,retrieve,de1ete](insert(s,d,k)), where “insert(s,d,k)” executes the insert action, and the instantiation of the non_empty_state process makes the object leave the empty state and enter the non_empty state. In the specifications of both empty_state and non_empty_state processes, sort S, which includes all the data values relevant to a Storage object, is formalized as a process parameter. The “insert(s,d,k)” Operation of sort S, which formalizes the insert action, inserts the newly received data associated with its key into the storage space and thereby derives the updated storage. The result of this action is that the storage is no longer empty. Consequently, the non_empty_state process is instantiated with parameter “insert (8 ,d,k))” that represents a non-empty storage object. 5.2.7 Summary. So far, we have addressed the formalization of the state diagram for an individual object. Objects that consist of an aggregation of objects are modeled by parallel composition constructs, addressed in the following discussion. 5.3 A tyr isinn ered < statet I] p059 ] opera 86 5.3 Concurrent State Formalization A typical system is usually composed of concurrent subsystems. In a system that is implemented by an object-oriented approach, the objects can always be consid- ered concurrent. In OMT, this concurrency is modeled as aggregate concurrency; in statecharts, it is modeled with AND states. The parallel composition operators of LOTOS provide sufficient semantics to com- pose parallel and concurrent processes. There are three types of parallel composition operators: 0 Full interleaving: No communication and synchronization between processes. 0 Full synchronization: Every action must be synchronized. 0 Normal synchronization: Only a select set of actions are synchronized. In the previous sections, we have shown that the formalization of the object and the dynamic models are inter-related by attributes, operations, events, gates, and state transitions. Similarly, the formalization of the concurrent composition in the state diagram is related to the aggregation associations that are identified and specified in the object diagrams. Theoretically, all the objects in a system are concurrent. In order to manage large, complex systems, we advocate a hierarchical approach to modeling the concurrent behavior that follows the system structure described in the object diagrams. The following rules describe the relationship between the aggregation relationship in the object model and the synchronization in the dynamic model. DfR-l Dill-l DfR-l S}r1( eurre sync] in te servi Slall Sert' ”Tide of ti Ber-l, ‘1 .‘.¥ in}: 87 DFR-14 Every aggregate object is responsible for composing the behavior of its concurrent aggregation objects to form one behavior specification. DFR—l5 The behavior of every aggregation Object must be composed by and only by its aggregate Object. DER-16 Only when there is an association between two aggregation objects, can the aggregate Object model the corresponding synchronization between the two objects. Synchronization mechanism and notations. The synchronization between con- current object dynamic models are specified by name binding. If two dynamic models, synchronized in a state diagram, share a common service, which is described as a gate in terms of LOTOS, the two dynamic models are synchronized through the shared service. The services (gates) modeled in the dynamic models for individual Objects can be considered as parameterized services. When an object is composed with other concurrent objects in parallel, the names of its services can be substituted by ac- tual names in the composition state diagram, such as the one shown in Figure 5.9. The dynamic models that share common actual names of services are synchronized through the shared services. In OMT, dashed lines are used to separate concurrent dynamic models in a given state diagram. If two concurrent dynamic models in a state diagram share no common service, they are composed in terms of interleaved LOTOS process algebras. However, under some circumstances, even if two dynamic models share common services, we still want to compose them as interleaving dynamic models. This happens when both of the objects use the same actual service to synchronize with objects other than each other. A new notation is introduced to represent the forced interleaving. The notation has three parallel lines drawn in vertical to the dashed line that separates the inter dtnamie The 1' that onlj 88 the interleaving dynamic models. A sample diagram is given in Figure 5.8, where dynamic models d2 and d3 are interleaved. O f... d2 d3 ———————— l bud—--I-Ifl—“a—‘n-H L Figure 5.8: A sample state diagram with interleaving dynamic models p. _ j The following rules use LOTOS’ normal synchronization construct [21] indicating that only a selected set of gates are synchronized. ln tl 0f Slam and am: Sptejfifa 89 DFR—l7 In a state diagram that composes dynamic models of concurrent objects, the dynamic behaviors are synchronized through shared services. The state diagram D = (S, 2, A, A, Q,C,E, i/J,)\,6, 90, C, so,c0) composed of D1=(51,21,A1,A1,4’1,01,31,1/J1,/\1,51,‘P1,Ci,810,C0), Dz = (52,£2,A2,A2.‘1’2,Cz,52,1l’2,A2r52,¢2,C2,320,CO), ------ r and Bu 2 (Sn,2,,,A,,,An,Qn,C,,,E,,,i/Jn,/\n,6,,,gon,cn,sno,c0) is formalized as: specification DESI U 22 U U 2,. U E] (x:¢,x1:¢1,x2 d2 , . . . ,xn:d>,,): noexit (algebraic specification> behaviour 80 [SUE] (X) | [T1] | (D1[21 U 51] (X1) I [T2] | (Dz [22 U 32] (X2) I [T3] | ( ..... | [Tn] l Dn [2,, U 3,] (x,,) D) where (process definitions) endspec, where T1, T2, ..., Tn are shared services. DFR-18 In a state diagram, the interleaving dynamic models are grouped together in terms of LOTOS interleaving process algebras. Ifstate diagrams DI =(51,21,A1,A1,¢1,CI.31.¢1,A1,51,991,C1,810,CO), Dz = (52,532,1)2,Amq’erczfizrll’z,A2,52,