Automated verification of design patterns with LePUS3

Jonathan Nicholson, Epameinondas Gasparis, Amnon Eden, Rick Kazman

Research output: Chapter in Book/Conference proceeding with ISSN or ISBNConference contribution with ISSN or ISBN

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 languageEnglish
Title of host publicationProceedings of the 1st NASA Formal Methods Symposium–NFM 2009
Pages76-85
Number of pages10
Publication statusPublished - Apr 2009
EventProceedings of the 1st NASA Formal Methods Symposium–NFM 2009 - Moffett Field, CA, USA
Duration: 1 Apr 2009 → …

Conference

ConferenceProceedings of the 1st NASA Formal Methods Symposium–NFM 2009
Period1/04/09 → …

Keywords

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

Fingerprint Dive into the research topics of 'Automated verification of design patterns with LePUS3'. Together they form a unique fingerprint.

Cite this