Verification of a radio-based signaling system using the STATEMATE verification environment

被引：31
作者：
Damm, W
Klose, J
机构：
[1] OFFIS, Oldenburg, Germany
[2] Univ Oldenburg, Dept Comp Sci CvO, D-2900 Oldenburg, Germany
来源：
FORMAL METHODS IN SYSTEM DESIGN | 2001年 / 19卷 / 02期
关键词：
STATEMATE; model-based design; radio-based signaling systems; formal verification; live sequence charts;
D O I：
10.1023/A:1011279932612
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
With the trend to partially move safety-related features from courtyards into on-board control software, new challenges arise in supporting such designs by formal verification capabilities, essentially entailing the need for a model-based design process. This paper reports on the usage of the STATEMATE Verification Environment to model and verify a radio-based signaling system, a trial case study offered by the German train system company DB. It shows, that industrially sized applications can be modeled and verified with a verification tool to be offered as a commercial product by I-Logix, Inc.
引用
收藏
页码：121 / 141
页数：21
相关论文
共 28 条
[11]   Model checking large software specifications [J].
Chan, W ;
Anderson, RJ ;
Beame, P ;
Burns, S ;
Modugno, F ;
Notkin, D ;
Reese, JD .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1998, 24 (07) :498-520
[12]  
Cimatti A., 1998, Formal Aspects of Computing, V10, P361, DOI 10.1007/s001650050022
[13]  
DAMM W, 1999, FMOODS 99 IFIP TC6 W
[14]  
DAMM W, 1998, LECT NOTES COMPUTER
[15]  
FESSLER M, 1999, FORM TECHN EIS FORMS
[16]  
Feyerabend K, 1997, LECT NOTES COMPUT SC, V1231, P156
[17]  
FEYERABEND K, 1996, REALTIME SYMBOLIC TI
[18]  
Fokkink W., 1998, P 3 WORKSH FORM METH
[19]  
GROOTE JF, 1995, P 10 IEEE C COMP ASS, P131
[20]  
HAREL D, 1996, MODELING REA D110043
123