Software Specification Methods: An Overview Using a Case StudyMarc Frappier, Henri Habrias Springer Science & Business Media, 6. dets 2012 - 282 pages Objectives of this Book This book is an introduction to a set of software specification methods. Its tar geted audience are readers who do not wish to read pages of definitions in order to understand the basics of a method. The same case study is used to introduce each method, following a rigorously uniform presentation format. Special care has been devoted to ensure that specifications do not deviate from the case study text. As much as the method allows, what is specified is what appears in the case study text. The benefits are two-fold. First, the reader can easily switch from one method to another, using his knowledge of the case study as a leverage to understand a new method. Second, it becomes easier to compare methods, because the same behavior is specified in each case. Each method presentation follows the same pattern. The concepts are pro gressively introduced when they are needed. To illustrate the specification pro cess, questions that the specifier should raise during the analysis of the case study are stated. Answers are provided as if they were given by an imaginary client. The question/answer process guides the derivation of the specification. Interestingly, the questions raised depend on the method, which is illustrative of the differences between them. |
Contents
9 | |
11 | |
Validation of the Specification | 16 |
8 | 18 |
4 | 36 |
3 | 49 |
Philippe Facon Régine Laleau Hong Phuong Nguyen | 56 |
3 | 66 |
3 | 120 |
4 | 128 |
3 | 137 |
4 | 143 |
9 | 147 |
4 | 162 |
Marc Frappier Richard StDenis | 191 |
Algebraic Specification in CASL | 209 |
4 | 74 |
2 | 82 |
3 | 88 |
6 | 91 |
69 | 97 |
4 | 111 |
References | 224 |
A Graphical Tool for System Modelling | 241 |
A Formal yet Expressive | 258 |
Index | 279 |
Other editions - View all
Common terms and phrases
abstract abstract machine action system Answer associated assume attribute behaviour cancel an order cancel order class diagram Collaboration diagram components constraints corresponding data types defined deletion domain entity entry error Estelle formal methods formal specification function definition given Hardware Description Language implementation initialisation instance interaction interface invariant invoice an order invoiced orders Invoicing1 language LOTOS maxorders method natural numbers neword notation object diagram operation invoice_order Order cancellation order is invoiced Order module order number order ProductRel order status ordered product ordered quantity Ordered_Qty OrderId output parameters pending orders Petri nets possible postconditions precondition predicate proof obligations provides quantity in stock Question 9 resp scenario schema semantics sequence sequence diagram set of orders signal SSADM State_of_stock state/transition diagrams stock level Stock module structure transition triggers update user requirements valid variable VHDL Z notation