Research Repository

Automated Verification of Design Patterns with LePUS3

Nicholson, Jonathan and Gasparis, Epameinondas and Eden, Amnon H and Kazman, Rick (2009) 'Automated Verification of Design Patterns with LePUS3.' In: Denny, Ewen and Giannakopolou, Dimitra and Pasareanu, Corina S, (eds.) Proceedings of the 1st NASA Formal Methods (NFM) Symposium. NASA, pp. 76-85.


Download (2MB) | Preview


Specification and [visual] modelling languages are expected to combine strong abstraction mechanisms with rigour, scalability, and parsimony. LePUS3 is a visual, object-oriented design description language axiomatized in a decidable subset of the first-order predicate logic. We demonstrate how LePUS3 is used to formally specify a structural design pattern and prove (‗verify‘) whether any JavaTM 1.4 program satisfies that specification. We also show how LePUS3 specifications (charts) are composed and how they are verified fully automatically in the Two-Tier Programming Toolkit.

Item Type: Book Section
Additional Information: proceedings of the First NASA Formal Methods Symposium (NFM 2009), held at the NASA Ames Research Center, in Moffett Field, CA, USA, on April 6 – 8, 2009.
Uncontrolled Keywords: specification; automated verification; visual languages; design description languages; object-oriented design
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Divisions: Faculty of Science and Health > Computer Science and Electronic Engineering, School of
Depositing User: Users 161 not found.
Date Deposited: 06 Aug 2012 13:52
Last Modified: 06 Aug 2012 13:52

Actions (login required)

View Item View Item