Software Specification Methods: An Overview Using a Case Study
Springer London, 2001 - 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.
What people are saying - Write a review
We haven't found any reviews in the usual places.
A Formal Specification Notation
SSADM Version 4 and
A ModelBased Method Using Generalised
13 other sections not shown
Other editions - View all
abstract action action system Actors added allows amount analysis Answer approach associated assume attribute behaviour called cancel colour communication components Computer consider constraints corresponding created defined definition deleted described diagram element entity entry error event example execution exist expressed Figure formal function give given identifier implementation includes initial input instance interaction introduced invoiced invoiced orders language loop Lotos machine marking means method module natural nets notation object object diagram occur operation ordered quantity output parameters pending orders Petri places possible precondition predicate proof properties provides quantity quantity in stock Question reference removed represented requirements response result satisfied scenarios schema sequence set of orders signal sort specification status structure tion tokens transition update valid variable verification