Verification of a Radio-Based Signaling System Using the STATEMATE Verification Environment

被引：0
|
作者：
Werner Damm
Jochen Klose
机构：
[1] OFFIS,Dept. of Computer Science C.v.O.
[2] Universität Oldenburg,undefined
来源：
Formal Methods in System Design | 2001年 / 19卷
关键词：
STATEMATE; model-based design; radio-based signaling systems; formal verification; live sequence charts;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
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
页数：20
相关论文
共 50 条
  • [1] Verification of a radio-based signaling system using the STATEMATE verification environment
    Damm, W
    Klose, J
    FORMAL METHODS IN SYSTEM DESIGN, 2001, 19 (02) : 121 - 141
  • [2] A Formal Verification Environment for Railway Signaling System Design
    Cinzia Bernardeschi
    Alessandro Fantechi
    Stefania Gnesi
    Salvatore Larosa
    Giorgio Mongardi
    Dario Romano
    Formal Methods in System Design, 1998, 12 : 139 - 161
  • [3] A formal verification environment for railway signaling system design
    Bernardeschi, C
    Fantechi, A
    Gnesi, S
    Larosa, S
    Mongardi, G
    Romano, D
    FORMAL METHODS IN SYSTEM DESIGN, 1998, 12 (02) : 139 - 161
  • [4] Implementation and verification of a digital radio communication system simulator for railway environment
    Kawasaki, Kunihiro
    Sugahara, Hiroyuki
    Tateishi, Yukiya
    Hattori, Tetsunori
    IEEJ Transactions on Industry Applications, 2015, 135 (04) : 420 - 425
  • [5] City implements radio-based system
    Water & Wastewater International, 2000, 15 (02):
  • [6] Implementation of a large, radio-based SCADA system
    Mozer, R
    Finnan, K
    ENTELEC '96, TECHNICAL PAPERS: TO EDUCATE AND INFORM, 1996, : 289 - 294
  • [7] VESTA: a system level verification environment based on C++
    Shahdadpuri, M
    Sosa, J
    Navarro, H
    Montiel-Nelson, JA
    Sarmiento, R
    VLSI CIRCUITS AND SYSTEMS, 2003, 5117 : 209 - 219
  • [8] Observer-based verification using introspection - A system-level verification implementation
    Metzger, M.
    Bastien, F.
    Rousseau, F.
    Vachon, J.
    Aboulhamid, E. M.
    ADVANCES IN DESIGN AND SPECIFICATION LANGUAGES FOR EMBEDDED SYSTEMS, 2007, : 209 - +
  • [9] Formal Verification of a Fuzzy Rule-Based Classifier Using the Prototype Verification System
    Gebreyohannes, Solomon
    Karimoddini, Ali
    Homaifar, Abdollah
    Esterline, Albert
    FUZZY INFORMATION PROCESSING, NAFIPS 2018, 2018, 831 : 1 - 12
  • [10] Verification of Dependable Architecture based on Prototype Verification System
    Yuan, Ling
    Fan, Ping
    PROCEEDINGS OF THE 2ND INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION APPLICATIONS (ICCIA 2012), 2012, : 918 - 921
12345