Verification of a Radio-Based Signaling System Using the STATEMATE Verification Environment |
| |
Authors: | Werner Damm Jochen Klose |
| |
Affiliation: | (1) OFFIS, Germany;(2) Dept. of Computer Science C.v.O., Universität Oldenburg, Germany |
| |
Abstract: | 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. |
| |
Keywords: | STATEMATE model-based design radio-based signaling systems formal verification live sequence charts |
本文献已被 SpringerLink 等数据库收录! |
|