The key approach:: Integrating object oriented design and formal verification

被引：11

作者：

Ahrendt, W

Baar, T

Beckert, B

Giese, M

Habermalz, E

Hähnle, R

Menzel, W

Schmitt, PH

机构：

[1] Univ Karlsruhe, Inst Log Complex & Deduct Syst, D-76128 Karlsruhe, Germany

[2] Chalmers Univ Technol, Dept Comp Sci, S-41296 Gothenburg, Sweden

来源：

LOGICS IN ARTIFICIAL INTELLIGENCE | 2000年 / 1919卷

关键词：

D O I：

10.1007/3-540-40006-0_3

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

This paper reports on the ongoing KeY project aimed at bridging the gap between (a) object-oriented software engineering methods and tools and (b) deductive verification. A distinctive feature of our approach is the use of a commercial CASE tool enhanced with functionality for formal specification and deductive verification.

引用

页码：21 / 36

页数：16

共 31 条

[1]

Abrial J., 2005, The B-book: Assigning Programs to Meanings

[2]

[Anonymous], OBJECT ORIENTED METH

[3]

[Anonymous], OBJECT TECHNOLOGY SE

[4]

APT KR, 1981, ACM T PROGRAMMING LA

[5]

BAAR T, 2000, UNPUB EXPERIENCES UM

[6]

BAAR T, 2000, SOFTWARETECHNIK TREN

[7]

BECKERT B, 2000, P 2 ECOOP WORKSH FOR

[8]

BORGER E, 1999, LNCS, V1523, P353

[9]

BREU R, 1997, P WORKSH PREC SEM OB

[10] Formal methods: State of the art and future directions [J].

Clarke, EM ;

Wing, JM .

ACM COMPUTING SURVEYS, 1996, 28 (04) :626-643

← 1 2 3 4 →