Research Repository

Automated verification of design patterns: A case study

Nicholson, Jon and Eden, Amnon H and Gasparis, Epameinondas and Kazman, Rick (2014) 'Automated verification of design patterns: A case study.' Science of Computer Programming, 80 (Part B). pp. 211-222. ISSN 0167-6423

Full text not available from this repository.


Representing design decisions for complex software systems, tracing them to code, and enforcing them throughout the lifecycle are pressing concerns for software architects and developers. To be of practical use, specification and modeling languages for software design need to combine rigor with abstraction and simplicity, and be supported by automated design verification tools that require minimal human intervention. This paper examines closely the use of the visual language of Codecharts for representing design decisions and demonstrate the process of verifying the conformance of a program to the chart. We explicate the abstract semantics of segments of the Java package java.awt as a finite structures, specify the Composite design pattern as a Codechart and unpack it as a set of formulas, and prove that the structure representing the program satisfies the formulas. We also describe a set of tools for modeling design patterns with Codecharts and for verifying the conformance of native (plain) Java programs to the charts.

Item Type: Article
Uncontrolled Keywords: Object-oriented design; Modeling and specification; Automated verification; Visual languages; Design description languages
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Divisions: Faculty of Science and Health > Computer Science and Electronic Engineering, School of
SWORD Depositor: Elements
Depositing User: Elements
Date Deposited: 05 Aug 2013 15:28
Last Modified: 06 Jan 2022 14:38

Actions (login required)

View Item View Item