Designing and Documenting the Behavior of Software


Gülesir, Gürcan and Bergmans, Lodewijk and Aksit, Mehmet (2007) Designing and Documenting the Behavior of Software. In: Remco van Engelen & Jeroen Voeten (Eds.), Ideals: evolvability of software-intensive high-tech systems : a collaborative research project on maintaining complex embedded systems. Embedded Systems Institute, Eindhoven, pp. 113-126. ISBN 9789078679035

open access
Abstract:The development and maintenance of today's software systems is an increasingly effort-consuming and error-prone task. A major cause of this problem is the lack of formal and human-readable documentation of software design. In practice, software design is often informally documented (e.g. texts in a natural language, `boxes-and-arrows' diagrams without well-defined syntax and semantics, etc.), or not documented at all. Therefore, the design cannot be properly communicated between software engineers, it cannot be formally analyzed, and the conformance of an implementation to the design cannot be formally verified.

In this chapter, we address this problem for the design and documentation of the behavior implemented in procedural programs. We introduce a solution that consists of three components: The first component is a graphical language called VisuaL, which enables engineers to specify constraints on the possible sequences of function calls from a given program. Since the specifications may be inconsistent with each other, the second component of our solution is a tool called CheckDesign, which automatically
verifies the consistency between multiple specifications written in VisuaL. The third component is a tool called CheckSource, which automatically verifies that a given implementation conforms to the corresponding specifications written in VisuaL.

This solution has been evaluated empirically through controlled experiments with 71 participants: 23 professional developers of ASML, and 49 Computer Science M.Sc. students. These experiments showed that, with statistical significance of 0.01, the solution reduced the effort of typical maintenance tasks by 75% and
prevented one error per 140 lines of source code.
Item Type:Book Section
Copyright:© 2007 Embedded Systems Institute
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 246025