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: 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
|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)
|Link to this item:||http://purl.utwente.nl/publications/60269|
|Export this item as:||BibTeX|
Daily downloads in the past month
Monthly downloads in the past 12 months
Repository Staff Only: item control page
Metis ID: 246025