Details

Software Specification Methods


Software Specification Methods


, Band 106 1. Aufl.

von: Henri Habrias, Marc Frappier

145,99 €

Verlag: Wiley
Format: PDF
Veröffentl.: 05.01.2010
ISBN/EAN: 9780470394656
Sprache: englisch
Anzahl Seiten: 418

DRM-geschütztes eBook, Sie benötigen z.B. Adobe Digital Editions und eine Adobe ID zum Lesen.

Beschreibungen

This title provides a clear overview of the main methods, and has a practical focus that allows the reader to apply their knowledge to real-life situations. The following are just some of the techniques covered: UML, Z, TLA+, SAZ, B, OMT, VHDL, Estelle, SDL and LOTOS.
<p><i>Preface vii</i></p> <p><i>List of Contributors xxiii</i></p> <p><b>Part I State-Based Approaches 1</b></p> <p><b>1 Z 3</b><br /> <i>Jonathan P. Bowen</i></p> <p>1.1 Overview of the Z notation 3</p> <p>1.1.1 The process of producing a Z specification 4</p> <p>1.2 Analysis and specification of case 1 5</p> <p>1.3 Analysis and specification of case 2 13</p> <p>1.4 Validation of the specification 16</p> <p>1.5 The natural language description of the specifications 18</p> <p>1.6 Conclusion 18</p> <p><b>2 SAZ 21</b><br /> <i>Fiona Polack</i></p> <p>2.1 Overview of the SAZ method 21</p> <p>2.2 Analysis and specification of case 1 22</p> <p>2.2.1 Z specification 24</p> <p>2.3 Analysis and specification of case 2 28</p> <p>2.4 Natural language description of the specifications 37</p> <p>2.4.1 Case 1 37</p> <p>2.4.2 Case 2 37</p> <p>2.5 Conclusions 38</p> <p><b>3 B 41</b><br /> <i>Hassan Diab and Marc Frappier</i></p> <p>3.1 Overview of the B notation 41</p> <p>3.2 Analysis and specification of case 1 42</p> <p>3.2.1 Identifying operations 42</p> <p>3.2.2 Defining the state space 44</p> <p>3.2.3 Defining the behavior of the invoicing operation 46</p> <p>3.2.4 The Product1 machine 49</p> <p>3.3 Analysis and specification of case 2 51</p> <p>3.3.1 Identifying operations 51</p> <p>3.3.2 The Product2 machine 51</p> <p>3.3.3 The Invoicing2 machine 52</p> <p>3.4 Validation of the specification 54</p> <p>3.5 The natural language description of the specifications 55</p> <p>3.5.1 Case 1 55</p> <p>3.5.2 Case 2 55</p> <p>3.6 Conclusion 56</p> <p><b>4 From UML Diagrams to B Specifications 59</b><br /> <i>Régine Laleau and Amel Mammar</i></p> <p>4.1 Overview of the method 59</p> <p>4.1.1 Summary of the B method 59</p> <p>4.1.2 Data specification 60</p> <p>4.1.3 Transaction specification 61</p> <p>4.2 Specification of case 1 64</p> <p>4.2.1 The class diagram and its B representation 64</p> <p>4.2.2 Transaction specification 66</p> <p>4.3 Specification of case 2 69</p> <p>4.3.1 Transactions specification 69</p> <p>4.3.2 The formal specification 72</p> <p>4.4 Validation 76</p> <p>4.5 The natural-language description of the specifications 77</p> <p>4.5.1 Case 1 77</p> <p>4.5.2 Case 2 77</p> <p>4.6 Conclusion 77</p> <p><b>5 UML+Z: Augmenting UML with Z 81</b><br /> <i>Nuno Amálio, Fiona Polack, and Susan Stepney</i></p> <p>5.1 Overview of UML+ Z 81</p> <p>5.2 Analysis and specification of case 1 82</p> <p>5.2.1 UML class model 82</p> <p>5.2.2 UML state models 83</p> <p>5.2.3 The Z model 84</p> <p>5.2.4 Checking model consistency 88</p> <p>5.2.5 Validating the model 89</p> <p>5.3 Analysis and specification of case 2 90</p> <p>5.3.1 Entries of new orders 90</p> <p>5.3.2 Cancellation of orders 94</p> <p>5.3.3 Entries of quantities into stock 96</p> <p>5.4 Natural language description of the specification 101</p> <p>5.4.1 Case 1 101</p> <p>5.4.2 Case 2 101</p> <p>5.5 Conclusion 101</p> <p><b>6 ASM 103</b><br /> <i>Egon Börger, Angelo Gargantini and Elvinia Riccobene</i></p> <p>6.1 Overview of the ASM 103</p> <p>6.2 Requirements capture and specification of case 1 104</p> <p>6.2.1 Identifying the agents 104</p> <p>6.2.2 Identifying the states 105</p> <p>6.2.3 Identifying static and dynamic parts of the states 105</p> <p>6.2.4 Identifying the transitions 107</p> <p>6.2.5 Identifying the initial and final states 111</p> <p>6.2.6 Exceptions handling and robustness 111</p> <p>6.2.7 Identifying the desired properties (validation/verification) 112</p> <p>6.3 Requirements capture and specification of case 2 114</p> <p>6.4 The natural language description of the specification 118</p> <p>6.4.1 Case 1 118</p> <p>6.4.2 Case 2 118</p> <p>6.5 Conclusion 118</p> <p><b>7 TLA+ 121</b><br /> <i>Leslie Lamport</i></p> <p>7.1 Overview of TLA+ 121</p> <p>7.1.1 TLA 121</p> <p>7.1.2 TLA+ versus Z 122</p> <p>7.2 A specification of case 2 124</p> <p>7.3 The problematic case 1 131</p> <p>7.4 Validation of the specification 132</p> <p>7.5 Satisfying the specification 133</p> <p>7.6 The natural language description 134</p> <p>7.7 Conclusion 134</p> <p><b>Part II Event-Based Approaches 137</b></p> <p><b>8 Action Systems 139</b><br /> <i>Jane Sinclair</i></p> <p>8.1 Overview of action systems 139</p> <p>8.2 Analysis and specification of case 1 140</p> <p>8.2.1 Modeling the state of the action system 140</p> <p>8.2.2 Defining the actions 143</p> <p>8.2.3 An action system for case 1 146</p> <p>8.3 Analysis and specification of case 2 147</p> <p>8.3.1 Modeling the state for case 2 147</p> <p>8.3.2 Defining the actions 147</p> <p>8.3.3 An action system for case 2 150</p> <p>8.4 Verification for action systems 151</p> <p>8.5 The natural language description of the specification 153</p> <p>8.5.1 Case 1 153</p> <p>8.5.2 Case 2 153</p> <p>8.6 Conclusion 153</p> <p><b>9 Event B 157</b><br /> <i>Dominique Cansell and Dominique Méry</i></p> <p>9.1 Introduction 157</p> <p>9.2 Analyzing the text of the case study 158</p> <p>9.3 Event-based modeling 164</p> <p>9.4 Modeling the first event B model Case 1 167</p> <p>9.5 Model refinement 170</p> <p>9.6 Modeling the second event B model Case 2 by refinement of Case 1 171</p> <p>9.7 The natural language description of the event B models 175</p> <p>9.8 Conclusion 175</p> <p><b>10 VHDL 179</b><br /> <i>Laurence Pierre</i></p> <p>10.1 Overview of VHDL 179</p> <p>10.2 Analysis and specification of case 1 181</p> <p>10.2.1 Identifying data structures 181</p> <p>10.2.2 Identifying operations 182</p> <p>10.3 Analysis and specification of case 2 186</p> <p>10.4 The natural language description of the specification 193</p> <p>10.4.1 Case 1 193</p> <p>10.4.2 Case 2 194</p> <p>10.5 Conclusion 194</p> <p><b>11 Estelle 197</b><br /> <i>Eric Lallett and Jean-Luc Raffy</i></p> <p>11.1 Overview of the FDT Estelle 197</p> <p>11.2 Analysis and specification of case 1 198</p> <p>11.2.1 Defining the architecture of the specification 198</p> <p>11.2.2 Defining the behavior 200</p> <p>11.3 Analysis and specification of case 2 204</p> <p>11.3.1 Defining the new architecture 204</p> <p>11.3.2 Defining the behavior 205</p> <p>11.4 Validating the specification 210</p> <p>11.5 The natural language description of the specifications 210</p> <p>11.5.1 Case 1 210</p> <p>11.5.2 Case 2 210</p> <p>11.6 JEstelle (Estelle with Java) 212</p> <p>11.7 Conclusion 212</p> <p><b>12 SDL 215</b><br /> <i>Pascal Poizat</i></p> <p>12.1 Overview of SDL 215</p> <p>12.2 Analysis and specification of case 1 216</p> <p>12.2.1 System structure 216</p> <p>12.2.2 Process graphs 219</p> <p>12.2.3 Sort definitions 221</p> <p>12.2.4 Comments on the first case study 225</p> <p>12.3 Analysis and specification of case 2 225</p> <p>12.3.1 System structure 225</p> <p>12.3.2 Process graphs 227</p> <p>12.3.3 Sort definitions 228</p> <p>12.4 The natural language description of the specifications 230</p> <p>12.4.1 Case 1 230</p> <p>12.4.2 Case 2 230</p> <p>12.5 Conclusion 230</p> <p><b>13 E-LOTOS 233</b><br /> <i>Kenneth J. Turner and Mihaela Sighireanu</i></p> <p>13.1 Overview of the LOTOS notation and method 233</p> <p>13.1.1 The LOTOS and E-LOTOS languages 233</p> <p>13.1.2 Requirements capture in LOTOS 234</p> <p>13.2 Analysis and specification of case 1 236</p> <p>13.2.1 Analysis 236</p> <p>13.2.2 Specification 237</p> <p>13.3 Analysis and specification of case 2 237</p> <p>13.3.1 Analysis 238</p> <p>13.3.2 Specification 242</p> <p>13.4 Validation and verification of the LOTOS specifications 250</p> <p>13.4.1 Validation 250</p> <p>13.4.2 Verification 251</p> <p>13.5 Natural language description of the specifications 255</p> <p>13.5.1 Case 1 255</p> <p>13.5.2 Case 2 255</p> <p>13.6 Conclusion 255</p> <p><b>14 EB3 259</b><br /> <i>Frédéric Gervais, Marc Frappier and Richard St-Denis</i></p> <p>14.1 Introduction 259</p> <p>14.2 Analysis and specification of case 1 260</p> <p>14.2.1 Entity types and actions 260</p> <p>14.2.2 Process expressions 262</p> <p>14.2.3 Input-output rules 262</p> <p>14.3 Analysis and specification of case 2 263</p> <p>14.3.1 Entity types, associations and actions 263</p> <p>14.3.2 Process expressions 266</p> <p>14.3.3 Input-output rules 268</p> <p>14.3.4 Attribute definitions 268</p> <p>14.4 The natural language description of the specification 271</p> <p>14.4.1 Case 1 271</p> <p>14.4.2 Case 2 272</p> <p>14.5 Conclusion 272</p> <p><b>Part III Other Formal Approaches 275</b></p> <p><b>15 CASL 277</b><br /> <i>Hubert Baumeister and Didier Bert</i></p> <p>15.1 Overview of the CASL notation 277</p> <p>15.2 Analysis and specification of case 1 278</p> <p>15.3 Analysis and specification of case 2 283</p> <p>15.4 Architectural specification 289</p> <p>15.5 The natural language description of the specification 290</p> <p>15.5.1 Case 1 290</p> <p>15.5.2 Case 2 290</p> <p>15.6 Conclusion 291</p> <p><b>16 Coq 293</b><br /> <i>Philippe Chavin and Jean-Francǫis Monin</i></p> <p>16.1 Introduction to Coq 293</p> <p>16.2 Analysis of the text 294</p> <p>16.2.1 Stock and orders 294</p> <p>16.2.2 Operations 295</p> <p>16.2.3 Requirements on quantities 296</p> <p>16.3 A specification for case1 296</p> <p>16.3.1 Basic types 296</p> <p>16.3.2 State and operation 298</p> <p>16.3.3 Operation “invoice” 298</p> <p>16.4 A specification for case2 300</p> <p>16.4.1 Using general operations over sets 300</p> <p>16.4.2 Reference-dependent measure systems 302</p> <p>16.5 Experimenting with the specification 304</p> <p>16.5.1 Refining 304</p> <p>16.6 Running an example 306</p> <p>16.7 Rephrasing the text 307</p> <p>16.8 Conclusion 308</p> <p><b>17 Petri Nets 311</b><br /> <i>Annie Choquet-Geniet and Pascal Richard</i></p> <p>17.1 Overview of Petrinets 311</p> <p>17.2 Analysis and specification of case 1 312</p> <p>17.2.1 One order with a data/action approach 313</p> <p>17.2.2 One order with a structural approach 316</p> <p>17.2.3 Several orders 319</p> <p>17.3 Analysis and specification of case 2 322</p> <p>17.3.1 Entry flow in stocks 322</p> <p>17.3.2 Flows of orders 323</p> <p>17.4 Validation of the specification 324</p> <p>17.5 The natural language description of the specifications 326</p> <p>17.5.1 Case 1 326</p> <p>17.5.2 Case 2 326</p> <p>17.6 Conclusion 326</p> <p><b>18 Petri Nets with Objects 329</b><br /> <i>Christophe Sibertin-Blanc</i></p> <p>18.1 Introduction 329</p> <p>18.2 A conceptual framework for the representation of systems 330</p> <p>18.3 Case 1 332</p> <p>18.4 The system’s interface 332</p> <p>18.5 The components of the system’s structure 333</p> <p>18.6 The Entities 335</p> <p>18.7 The Operations 338</p> <p>18.8 The Actors 339</p> <p>18.9 The Control Structure 340</p> <p>18.10 Natural language description of the specifications 345</p> <p>18.11 Comments about our treatment of the case study 346</p> <p><b>Part IV Comparison and Glossary 351</b></p> <p><b>19 A Comparison of the Specification Methods 353</b><br /> <i>Marc Frappier, Henri Habrias and Pascal Poizat</i></p> <p>19.1 Attributes of specification methods 353</p> <p>19.1.1 Paradigm 353</p> <p>19.1.2 Formality 356</p> <p>19.1.3 Graphical representation 357</p> <p>19.1.4 Object oriented 357</p> <p>19.1.5 Concurrency 357</p> <p>19.1.6 Executability 357</p> <p>19.1.7 Usage of variables 357</p> <p>19.1.8 Non-determinism 357</p> <p>19.1.9 Logic 358</p> <p>19.1.10 Provability 358</p> <p>19.1.11 Model checking 358</p> <p>19.1.12 Event inhibition 358</p> <p>19.2 A qualitative description of the methods 359</p> <p><b>20 Glossary 365</b><br /> <i>Henri Habrias, Pascal Poizat and Marc Frappier</i></p> <p><i>Index 411</i></p>
<b>Henri Habrias</b>, University of Nantes, France <p><b>Marc Frappier</b>, University of Sherbrooke, Canada</p>
This title provides a clear overview of the main methods, and has a practical focus that allows the reader to apply their knowledge to real-life situations. The following are just some of the techniques covered: UML, Z, TLA+, SAZ, B, OMT, VHDL, Estelle, SDL and LOTOS.

Diese Produkte könnten Sie auch interessieren:

MDX Solutions
MDX Solutions
von: George Spofford, Sivakumar Harinath, Christopher Webb, Dylan Hai Huang, Francesco Civardi
PDF ebook
53,99 €
Concept Data Analysis
Concept Data Analysis
von: Claudio Carpineto, Giovanni Romano
PDF ebook
99,99 €
Handbook of Virtual Humans
Handbook of Virtual Humans
von: Nadia Magnenat-Thalmann, Daniel Thalmann
PDF ebook
136,99 €