COLLECTIVE SPECIFICATION AND VERIFICATION OF BEHAVIOR MODELS AND OBJECT-ORIENTED IMPLEMENTATIONS

被引：0

作者：

Yi, Qing ^{[1
]}

Niu, Jianwei ^{[1
]}

Marneni, Anitha R. ^{[1
]}

机构：

[1] Univ Texas San Antonio, One UTSA Circle, San Antonio, TX 78249 USA

来源：

ICSOFT 2011: PROCEEDINGS OF THE 6TH INTERNATIONAL CONFERENCE ON SOFTWARE AND DATABASE TECHNOLOGIES, VOL 2 | 2011年

关键词：

Code generation; Modeling checking; Finite state machine;

D O I：

暂无

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We present a finite-state-machine-based language, iFSM, to seamlessly integrate the behavioral logic and implementation strategies of object-oriented abstractions and prevent them from being out-of-sync. We provide a transformation engine which automatically translates iFSM specifications to lower-level C++/Java class implementations that are similar in style to manually written code. Further, we automatically verify that these implementations are consistent with their behavior models by translating iFSM specifications into the input language of model checker NuSMV.

引用

页码：15 / 24

页数：10

共 50 条

[1] Collective specification and verification of behavior models and object-oriented implementations
Yi, Qing
Niu, Jianwei
Marneni, Anitha R.
[J]. ICSOFT 2011 - Proceedings of the 6th International Conference on Software and Database Technologies, 2011, 2 : 15 - 24
[2] Specification and Verification of Object-Oriented Software
Leino, K. Rustan M.
[J]. ENGINEERING METHODS AND TOOLS FOR SOFTWARE SAFETY AND SECURITY, 2009, 22 : 231 - 266
[3] MODULAR SPECIFICATION AND VERIFICATION OF OBJECT-ORIENTED PROGRAMS
LEAVENS, GT
[J]. IEEE SOFTWARE, 1991, 8 (04) : 72 - 80
[4] Specification and verification challenges for sequential object-oriented programs
Leavens, Gary T.
Leino, K. Rustan M.
Mueller, Peter
[J]. FORMAL ASPECTS OF COMPUTING, 2007, 19 (02) : 159 - 189
[5] SPECIFICATION AND VERIFICATION OF OBJECT-ORIENTED PROGRAMS USING SUPERTYPE ABSTRACTION
LEAVENS, GT
WEIHL, WE
[J]. ACTA INFORMATICA, 1995, 32 (08) : 705 - 778
[6] Object-oriented specification of models and experiments in traffic simulation
Mugge, H
Meyer, R
Hilty, LM
Page, B
[J]. ENVIRONMENTAL SOFTWARE SYSTEMS, VOL 2, 1997, : 335 - 342
[7] PRECISE SPECIFICATION OF BEHAVIOR IN OBJECT-ORIENTED STANDARDIZATION ACTIVITIES
KILOV, H
[J]. COMPUTER STANDARDS & INTERFACES, 1993, 15 (2-3) : 275 - 285
[8] Precise specification of behavior in object-oriented standardization activities
Kilov, Haim
[J]. Computer Standards and Interfaces, 1993, 15 (2-3): : 275 - 285
[9] AN OBJECT-ORIENTED SPECIFICATION FOR COMPILER
WU, PC
WANG, FJ
[J]. SIGPLAN NOTICES, 1992, 27 (01): : 85 - 94
[10] Unification and consistency verification of object-oriented analysis models
Aoki, T
Katayama, T
[J]. 1998 ASIA PACIFIC SOFTWARE ENGINEERING CONFERENCE, PROCEEDINGS, 1998, : 296 - 303

← 1 2 3 4 5 →