Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Software engineering : specification, implementation, verification
Alagić S., Springer International Publishing, New York, NY, 2017. 178 pp. Type: Book (978-3-319615-17-2)
Date Reviewed: Feb 1 2018

Many introductions to software engineering focus on the high-level aspects of large-scale software development, for example, requirements analysis, architecture design, configuration management, quality control, software maintenance, documentation, project management, and the like. The core process of how to actually produce software in such a way that it meets given requirements is often given comparably shallow treatment.

This textbook differs from such introductions in that it deals exactly with this core process. It presents a systematic software development approach that proceeds in multiple stages and revolves around formally specified software models. These models are expressed in the object constraint language (OCL), a part of the unified modeling language (UML) standard that allows logic constraints to precisely describe the expected behavior of objects and methods. Although the various kinds of graphical diagrams of the UML standard are usually treated in great detail, the logic-based OCL is often neglected; here, however, it represents the cornerstone of the presented approach.

The first three chapters lay the corresponding groundwork: chapter 1 introduces, through various examples, the use of different kinds of UML diagrams in the analysis and design phase of the software engineering process; a similar presentation can also be found in other software engineering textbooks. With chapter 2, however, well-trodden paths are left: the chapter presents the use of OCL in order to specify, with constraints, invariants for objects and pre- and post-conditions for methods; special emphasis is given to constraints over collections by describing quantification over collections, selection of collection elements by predicates, and resulting queries over collections. Then, chapter 3 gives an overview of modern implementation technologies, discussing the basic concepts of object-oriented programming as well as parametric polymorphism and concurrency. Such material is usually omitted in other presentations, but it makes the following material accessible also to novices.

The next three chapters represent the core of the book: chapter 4 discusses how the techniques presented so far can be used to construct, in a first step, OCL-annotated UML models that can be, in a second step, mapped to actual code in such a way that the specified constraints are satisfied. For two sample applications (investment management and course management), OCL-annotated interfaces are specified, which are then implemented by classes; as a specific feature of this approach, the classes operate on globally declared collections of objects that are intended to model “persistent” data, which is discussed later in more detail. A more elaborate flight management application gives the opportunity to present models with more complex constraints. A section is especially dedicated to the management of models and code by discussing model transformation, refactoring, forward engineering, and reverse engineering.

Chapter 5 continues by discussing data management, that is, how to maintain persistent objects whose lifetime extends beyond the activation of the program. It first describes in a generic fashion useful properties of such data representations, and then presents how they can be realized by various concrete Java-based technologies (file-based persistence by object serialization, the Java Data Objects model for persistence with transactions, and the Java Persistence application programming interface (API) technology for object-relational mappings). Chapter 6 finally discusses how the correctness of the developed code with respect to the specified OCL constraints can be verified. Actually, the chapter mainly focuses on the “Code Contracts” framework of the C# language, which just allows one to validate code at runtime by evaluating constraints; only the last section sketches static verification with the Spec# system, using a small stock market application as an example.

This textbook may serve as a nice companion to a first hands-on introduction to software engineering that focuses on how to produce abstract models that state application requirements and how to turn these models into code that meets these requirements. By relying mainly on examples to present its ideas, the book tries to be illustrative more than comprehensive and exact. By not relying on much prior knowledge, neither in formal logic nor in software development, the material stands on its own.

Since the presentation is thus (necessarily) sketchy, it should be considered as a first starting point for further study in various areas: the language and calculus of first-order logic (OCL constraints are just logic formulas in a peculiar syntax), formal specification and verification (necessary to understand the roles of object and loop invariants), object-oriented programming technology, and the (intentionally) omitted aspects of software engineering; for this purpose, the book includes also a (too) short section with an annotated list of references to some of these topics. Unfortunately, the book is not (yet?) accompanied by a Web site with concrete models or source code, which would allow readers to actually use and extend these. Despite these minor shortcomings, provided that the limits of the presentation are considered, the book can be fully recommended as a first introduction to the field of model-based software engineering.

Reviewer:  Wolfgang Schreiner Review #: CR145827 (1804-0161)
Bookmark and Share
  Featured Reviewer  
 
Software/ Program Verification (D.2.4 )
 
 
Logic And Constraint Programming (F.4.1 ... )
 
 
Requirements/ Specifications (D.2.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Software/Program Verification": Date
Verification of sequential and concurrent programs
Krzysztof R., Olderog E., Springer-Verlag New York, Inc., New York, NY, 1991. Type: Book (9780387975320)
Jul 1 1992
On verification of programs with goto statements
Lifschitz V. (ed) Information Processing Letters 18(4): 221-225, 1984. Type: Article
Mar 1 1985
The validation, verification and testing of software
Ince D. (ed), Oxford University Press, Inc., New York, NY, 1985. Type: Book (9789780198590040)
Sep 1 1987
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