The rhapsody UML verification environment

被引：34

作者：

Schinz, I ^{[1
]}

Toben, T ^{[1
]}

Mrugalla, C ^{[1
]}

Westphal, B ^{[1
]}

机构：

[1] Carl von Ossietzky Univ Oldenburg, D-26111 Oldenburg, Germany

来源：

PROCEEDINGS OF THE SECOND INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS | 2004年

关键词：

D O I：

10.1109/SEFM.2004.1347518

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Object-oriented modeling plays an increasing role in the design of embedded controllers. Formal verification can be applied in order to give evidence for meeting safety critical requirements. The "Rhapsody UML Verification Environment" supports verification of safety and liveness requirements for embedded controllers, developed within the Unified Modeling Language (UML). The verification environment is integrated in the design tool "Rhapsody in C++" offered by the company I-Logix. This paper discusses how UML models are transformed into a format usable for the VIS model checker, shows the specification and verification on a simple example and explains how the tool can be used to help determining the memory resources of a model.

引用

页码：174 / 183

页数：10

共 25 条

[1]

BOHN J, 1999, SMI SYSTEM MODELLING

[2]

Bozga M, 1999, LECT NOTES COMPUT SC, V1708, P307

[3]

Clarke EM, 1999, MODEL CHECKING, P1

[4] LSCs: Breathing life into message sequence charts [J].

Damm, W ;

Harel, D .

FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (01) :45-80

[5]

DAMM W, 2003, LNCS, V2852

[6]

Gery E., 2002, Integrated Formal Methods. Third International Conference, IFM 2002. Proceedings (Lecture Notes in Computer Science Vol.2335), P1

[7] Executable object modeling with statecharts [J].

Harel, D ;

Gery, E .

COMPUTER, 1997, 30 (07) :31-&

[8]

*IAI EADS NLR FTR, MOD SPEC CAS STUD UM

[9]

KLOSE J, 2002, P INT2002 INT WORKSH

[10]

KLOSE J, 2003, THESIS CARV VONOSSIE

← 1 2 3 →