Nicholson, Jonathan and Gasparis, Epameinondas and Eden, Amnon H and Kazman, Rick (2009) Automated Verification of Design Patterns with LePUS3. In: Proceedings of the 1st NASA Formal Methods (NFM) Symposium. NASA, pp. 76-85.
Nicholson, Jonathan and Gasparis, Epameinondas and Eden, Amnon H and Kazman, Rick (2009) Automated Verification of Design Patterns with LePUS3. In: Proceedings of the 1st NASA Formal Methods (NFM) Symposium. NASA, pp. 76-85.
Nicholson, Jonathan and Gasparis, Epameinondas and Eden, Amnon H and Kazman, Rick (2009) Automated Verification of Design Patterns with LePUS3. In: Proceedings of the 1st NASA Formal Methods (NFM) Symposium. NASA, pp. 76-85.
Abstract
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 |
| URI: | http://repository.essex.ac.uk/id/eprint/3488 |
Available files
Filename: nicholson_automated_2009.pdf