Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Formal specification level : concepts, methods, and algorithms
Soeken M., Drechsler R., Springer Publishing Company, Incorporated, Cham, Switzerland, 2015. 138 pp. Type: Book (978-3-319086-98-9)
Date Reviewed: Feb 20 2015

The genesis of every complex system is an informal set of requirements. In a good development process, these are formalized as a text document. This natural language text, however, is not truly formal; it is susceptible to being misunderstood and is difficult to analyze for contradictions and omissions. Through a series of steps, the requirements are transformed into formal artifacts such as source code and configuration files. The most difficult and error-prone part of the development process is the transition from informal to formal descriptions of the system.

The “formal specification level” of the book’s title isn’t new. It consists of unified modeling language (UML) or systems modeling language (SysML) models--specifically, class diagrams with object constraint language (OCL) invariants and pre- and post-conditions. What is new is the description of tools to assist the transition from natural language text into formal models, to verify that these models are consistent, and to transform them in various ways.

After some preliminaries (chapters 1 and 2), chapter 3 discusses the use of natural language processing (NLP) techniques such as part-of-speech tagging with word-sense disambiguation to generate formal models from unrestricted textual inputs. First, nouns are analyzed to find classes and actors. Then, attributes are extracted from adjectives and constant values (numbers and quoted words). Finally, operations are identified from verbs, and associations from prepositions. The result is a class diagram. OCL invariants are then added by translating the abstract syntax trees of parts of the text into OCL expressions with similar structure. The final model is of course only a draft and the developer can modify it as needed.

Once a model is available, the techniques of chapter 4 can be used to verify its consistency--that is, to ensure that an instance of the model exists. Several methods for checking consistency are discussed; the most efficient is a direct translation of the model to a Boolean formula that can be checked by a satisfiability modulo theories (SMT) solver. If the model is consistent, an instance can be generated. However, if it is inconsistent, it is necessary to find the core of the inconsistency--that is, the smallest subset of the model that exhibits the inconsistency. This will assist the developer in identifying the issue and resolving it. Several techniques for finding such a small (although not necessarily the smallest) subset are described.

The behavioral aspects of the model are described by pre- and post-conditions on operations. Chapter 5 extends the static verification techniques of the previous chapter to the dynamic case, with applications that discover deadlocks, livelocks, and operations that can never be executed. In addition, an algorithm that replaces some global invariants by equivalent pre- or post-conditions is described.

The proposed techniques cover an important part of the transformation from informal specifications or use case scenarios (rather than requirements) to formal models, and are a significant contribution to the research in this area. However, they have many limitations that need to be overcome before they can be used in practice. Most significant is the question of scalability. The book demonstrates the techniques on fairly small examples; how they will perform on large systems is still an open question. Also, the methods don’t address cycles in the development process: when specifications (or requirements) change after significant analysis and transformation activities have already been carried out, how can the effort be reused?

Furthermore, the algorithms given have various limitations. The weakest in my opinion are the NLP techniques of chapter 3. (This isn’t surprising given that this is the most challenging part of the transformation.) To give just a single example, the word “exact” in “the customer provides the exact price to the machine” is interpreted as an attribute of “price” (p. 51), although it is a relationship between the payment and the price.

As with other techniques based on satisfiability checking, the algorithms of chapters 4 and 5 require a bound on the search space to be given a priori. If the supplied bounds are too small, the solver may fail to find an instance of the model even though one may exist. The discussion in Section 4.5.2 about how to determine bounds automatically doesn’t solve this problem, since it can find minimum bounds but not, in general, maximum bounds.

The book is not easy to read: it has some very technical and formal parts and not enough examples and intuitive explanations of the algorithms, as well as some typographical errors and inconsistencies. For researchers working in this domain, however, it is a must-read. They will find the techniques described a valuable starting point for extension, or a standard against which to compare other efforts.

Reviewer:  Yishai Feldman Review #: CR143198 (1506-0442)
Bookmark and Share
  Reviewer Selected
Featured Reviewer
 
 
Requirements/ Specifications (D.2.1 )
 
 
Formal Methods (D.2.4 ... )
 
 
Real-Time And Embedded Systems (C.3 ... )
 
 
Special-Purpose And Application-Based Systems (C.3 )
 
Would you recommend this review?
yes
no
Other reviews under "Requirements/Specifications": Date

Moriconi M. (ed), Lansky A.Type: Article
Dec 1 1985
A unifying framework for structured analysis and design models
Tse T., Cambridge University Press, New York, NY, 1991. Type: Book (9780521391962)
Jun 1 1992
A skeleton interpreter for specialized languages
Steensgaard-Madsen J.  Programming Languages and System Design (, Dresden, East Germany,1861983. Type: Proceedings
Mar 1 1985
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy