| タイトル | Automated Verification of Design Patterns with LePUS3 |
| 本文（外部サイト） | http://hdl.handle.net/2060/20100024465 |
| 著者（英） | Eden, Ammon H.; Nicholson, Jonathan; Kazman, Rick; Gasparis, Epameinondas |
| 著者所属（英） | NASA Ames Research Center |
| 発行日 | 2009-04-01 |
| 言語 | eng |
| 内容記述 | 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. |
| NASA分類 | Mathematical and Computer Sciences (General) |
| 権利 | Copyright, Distribution as joint owner in the copyright |
| URI | https://repository.exst.jaxa.jp/dspace/handle/a-is/564274 |
