DLR-Logo -> http://www.dlr.de
DLR Portal Home | Imprint | Privacy Policy | Contact | Deutsch
Fontsize: [-] Text [+]

Test Case Generation for a Level Crossing Controller

Schwencke, Daniel (2020) Test Case Generation for a Level Crossing Controller. In: 2nd SmartRaCon Scientific Seminar, 37, pp. 89-98. 2nd SmartRaCon Scientific Seminar, 24. Nov. 2020, San Sebastian, Spanien / Webkonferenz. ISSN 1866-721X.

[img] PDF


Formal methods (FM) can be used for the precise specification, property-ensuring development and exhaustive property verification of systems. Thus they are especially suited for highly safety or mission critical applications. Railway signaling systems clearly belong to these applications, and there are indeed several industrial projects where FM have been successfully applied; especially to core interlocking and communication-based train control (CBTC) systems. But despite their potential, FM are not very wide-spread in the sector. Work Package 5 of the X2Rail-2 project seeks to foster the use of FM in railway signaling by providing an introduction and overview of formal methods and demonstrating their use and benefit. For the latter, four different formal and one classical development methods are applied by different project partners to a level crossing (LX) controller specified by the Swedish railway infrastructure manager Trafikverket. For all of these developments, the safety properties from the LX specification are planned to be formally verified afterwards using the High Level Language (HLL). Since that means proving them exhaustively, they are of less interest for testing. However, there are further non-safety functional requirements in the specification which remain for testing. The extended abstract at hand reports on an automatic test case generation (TCG) approach of a test suite testing these requirements. In fact, this approach is based on formal methods as well, since the test case generator applies symbolic execution and theorem solving techniques: given a behavioral model of the system under test (SUT), the former method finds feasible paths through the model, while the latter completes the test case by determining suitable test data. This way, the test design task is partly automated, ensures a structural coverage of the model and the modeling process usually leads to a high test suite quality. The different LX controller implementations are tested as black box systems, each one with the same generated test cases. In order to simplify the integration of the different implementations with the test environment, a common test interface has been drawn up.

Item URL in elib:https://elib.dlr.de/140046/
Document Type:Conference or Workshop Item (Speech)
Title:Test Case Generation for a Level Crossing Controller
AuthorsInstitution or Email of AuthorsAuthor's ORCID iD
Schwencke, DanielDaniel.Schwencke (at) dlr.dehttps://orcid.org/0000-0002-0592-9551
Date:November 2020
Journal or Publication Title:2nd SmartRaCon Scientific Seminar
Refereed publication:Yes
Open Access:Yes
Gold Open Access:No
In ISI Web of Science:No
Page Range:pp. 89-98
Series Name:Berichte aus dem DLR-Institut für Verkehrssystemtechnik
Keywords:test generation, level crossing controller, formal methods, Rhapsody
Event Title:2nd SmartRaCon Scientific Seminar
Event Location:San Sebastian, Spanien / Webkonferenz
Event Type:international Conference
Event Dates:24. Nov. 2020
HGF - Research field:Aeronautics, Space and Transport
HGF - Program:Transport
HGF - Program Themes:Rail Transport
DLR - Research area:Transport
DLR - Program:V SC Schienenverkehr
DLR - Research theme (Project):V - Digitalisierung und Automatisierung des Bahnsystems
Location: Braunschweig
Institutes and Institutions:Institute of Transportation Systems > Verification and Validation
Deposited By: Schwencke, Dr. Daniel
Deposited On:19 Apr 2021 09:54
Last Modified:20 Jun 2021 15:54

Repository Staff Only: item control page

Help & Contact
electronic library is running on EPrints 3.3.12
Copyright © 2008-2017 German Aerospace Center (DLR). All rights reserved.