A Formal Modeling Methodology Of The French
Railway Interlocking System Via HCPN
Author(s)
P. Sun, S. Collart-Dutilleul & P. Bon
Abstract
A railway interlocking system (RIS) plays a vital role in the safe transportation of
a railway system. It is responsible for the safe routes of trains making sure that
each train movement follows the other in a proper and safe sequence. Detailed
verifications and evaluations are mandatory before deploying an RIS, since it is
a safety critical system (SCS). But the increasing complexity of the RIS tends to
limit the capability of the classic approval methods. As a result, the formalization
of RIS becomes important to both the development of computer interlocking
software and the third-party testing of the RIS facilities. Petri nets are a powerful
formal tool that have been applied to many railway applications. Considering the
large scale and the space complexity of interlocking systems, this paper introduces
a feasible method for modeling the RIS by hierarchical colored Petri net (HCPN),
which aim at providing a formal verification and logic evaluation of the French
RIS. The paper describes how the signaling control logical and the railway road
layout are specified and constructed into the HCPN. First, the architecture of
RIS and the hierarchical structure of the model framework are introduced. Then,
several basic RIS components are established as Petri nets to illustrate how to
map RIS components into HCPN. As a case study, a section of a typical French
station is modeled. It includes interlocking routes and signaling control principles.
This paper takes place in the framework of the ANR project ‘PERFECT’. As this
method has already received recognition from French railway experts, the future
research contains consistency checking with some other parts of the specification,
such as operation rules, which allows us to find out the crux of some existing
problems and to discover some potential safety hazards.
Keywords: railway interlocking system, modeling methodology, hierarchical
colored Petri net.
Keywords
railway interlocking system, modeling methodology, hierarchical
colored Petri net.
Related Book
Other papers in this volume
Warning (2)
: foreach() argument must be of type array|object, null given [in
/var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/templates/Papers/view.php, line
364]
Code
$counter = '0';
foreach ($paper['book']['Paper'] as $otherPaper) {
if ((!empty($otherPaper['name'])) && ($counter < '7') && ($otherPaper['available'] == 1)) {
Cake\Error\ErrorTrap->handleError() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/templates/Papers/view.php, line 364
/var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/View/View.php /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/View/View.php, line 1188
Cake\View\View->_evaluate() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/View/View.php, line 1145
Cake\View\View->_render() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/View/View.php, line 785
Cake\View\View->render() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Controller/Controller.php, line 712
Cake\Controller\Controller->render() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Controller/Controller.php, line 516
Cake\Controller\Controller->invokeAction() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Controller/ControllerFactory.php, line 166
Cake\Controller\ControllerFactory->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Controller/ControllerFactory.php, line 141
Cake\Controller\ControllerFactory->invoke() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/BaseApplication.php, line 362
Cake\Http\BaseApplication->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 86
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Middleware/CsrfProtectionMiddleware.php, line 169
Cake\Http\Middleware\CsrfProtectionMiddleware->process() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 82
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Middleware/BodyParserMiddleware.php, line 157
Cake\Http\Middleware\BodyParserMiddleware->process() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 82
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Routing/Middleware/RoutingMiddleware.php, line 118
Cake\Routing\Middleware\RoutingMiddleware->process() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 82
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Routing/Middleware/AssetMiddleware.php, line 69
Cake\Routing\Middleware\AssetMiddleware->process() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 82
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Error/Middleware/ErrorHandlerMiddleware.php, line 115
Cake\Error\Middleware\ErrorHandlerMiddleware->process() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 82
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/debug_kit/src/Middleware/DebugKitMiddleware.php, line 60
DebugKit\Middleware\DebugKitMiddleware->process() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 82
Cake\Http\Runner->handle() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Runner.php, line 60
Cake\Http\Runner->run() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/vendor/cakephp/cakephp/src/Http/Server.php, line 104
Cake\Http\Server->run() /var/www/dce7ae55-385b-4ffa-8595-3ec5e61ff110/public_html/app/webroot/index.php, line 37
[main]
