Automated verification of design patterns with LePUS3

Jonathan Nicholson; Epameinondas Gasparis; Amnon Eden; Rick Kazman

Automated verification of design patterns with LePUS3

Jonathan Nicholson, Epameinondas Gasparis, Amnon Eden, Rick Kazman

University of Brighton

Research output: Chapter in Book/Conference proceeding with ISSN or ISBN › Conference contribution with ISSN or ISBN › peer-review

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.

Original language	English
Title of host publication	Proceedings of the 1st NASA Formal Methods Symposium–NFM 2009
Pages	76-85
Number of pages	10
Publication status	Published - Apr 2009
Event	Proceedings of the 1st NASA Formal Methods Symposium–NFM 2009 - Moffett Field, CA, USA Duration: 1 Apr 2009 → …

Conference

Conference	Proceedings of the 1st NASA Formal Methods Symposium–NFM 2009
Period	1/04/09 → …

Keywords

specification
automated verification
visual languages
design description languages
object-oriented design

Access to Document

http://shemesh.larc.nasa.gov/NFM2010/proceedings/NASA-CP-2009-215407.pdfLicence: Unspecified

Cite this

@inproceedings{e0c00f1bbfa749e5ae93674933bd22f0,

title = "Automated verification of design patterns with LePUS3",

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.",

keywords = "specification, automated verification, visual languages, design description languages, object-oriented design",

author = "Jonathan Nicholson and Epameinondas Gasparis and Amnon Eden and Rick Kazman",

year = "2009",

month = apr,

language = "English",

pages = "76--85",

booktitle = "Proceedings of the 1st NASA Formal Methods Symposium–NFM 2009",

note = "Proceedings of the 1st NASA Formal Methods Symposium–NFM 2009 ; Conference date: 01-04-2009",

}

TY - GEN

T1 - Automated verification of design patterns with LePUS3

AU - Nicholson, Jonathan

AU - Gasparis, Epameinondas

AU - Eden, Amnon

AU - Kazman, Rick

PY - 2009/4

Y1 - 2009/4

N2 - 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.

AB - 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.

KW - specification

KW - automated verification

KW - visual languages

KW - design description languages

KW - object-oriented design

M3 - Conference contribution with ISSN or ISBN

SP - 76

EP - 85

BT - Proceedings of the 1st NASA Formal Methods Symposium–NFM 2009

T2 - Proceedings of the 1st NASA Formal Methods Symposium–NFM 2009

Y2 - 1 April 2009

ER -

Automated verification of design patterns with LePUS3

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this