scholarly journals A Railway Scheduling Method using Probabilistic Model Checking

Trains scheduling is an important problem in railway transportation. Many companies use fixed train timetabling to handle this problem. Train delays can affect the pre-defined timetables and postpone destination arrival times. Besides, delay propagation may affect other trains and degrade the performance of a railway network. An optimal timetable minimizes the total propagated delays in a network. In this paper, we propose a new approach to compute the expected propagated delays in a railway network. As the main contribution of the work, we use Discrete-time Markov chains to model a railway network with a fixed timetable and use probabilistic model checking to approximate the expected delays and the probability of reaching destinations with a desired delay. We use PRISM model checker to apply our approach for analyzing the impact of different train scheduling in double line tracks.

2015 ◽  
pp. 831-844
Author(s):  
Jinyu Kai ◽  
Huaikou Miao ◽  
Kun Zhao ◽  
Jiaan Zhou ◽  
Honghao Gao

Service oriented software systems running in a highly open, dynamic and unpredictable Internet environment are inevitable to face all kinds of uncertainty. To monitor the operation of the web services system behavior analysis and analysis whether the system behavior is consistent with the requirements is the basis to determine whether the system needs to be reconfigured. In this paper, an analytical platform for the behavior of a web service-oriented system based on the probabilistic model checking is introduced which provides the basis for judging whether a system needs to be reconfigured by applying the approach of probabilistic model checking to verify whether the behavior system model is satisfied requirement properties. This platform is implemented in Java language and using the dot tool that the Graphviz provides and the PRISM model checker to construct the behavior model of the web service-oriented system based on web log files, to view and edit behavior models visually, and to convert the model from one form to another to make it convenience for users to use the model checker PRISM. Finally, we can judge whether the model is satisfied the desired requirements according to the verification result.


Author(s):  
Christel Baier ◽  
Clemens Dubslaff ◽  
Sascha Klüppelholz ◽  
Marcus Daum ◽  
Joachim Klein ◽  
...  

2016 ◽  
Vol 29 (2) ◽  
pp. 287-299 ◽  
Author(s):  
Shashank Pathak ◽  
Luca Pulina ◽  
Armando Tacchella

Author(s):  
Joachim Klein ◽  
Christel Baier ◽  
Philipp Chrszon ◽  
Marcus Daum ◽  
Clemens  Dubslaff ◽  
...  

Author(s):  
Anton Tarasyuk ◽  
Elena Troubitsyna ◽  
Linas Laibinis

Formal refinement-based approaches have proved their worth in verifying system correctness. Often, besides ensuring functional correctness, we also need to quantitatively demonstrate that the desired level of dependability is achieved. However, the existing refinement-based frameworks do not provide sufficient support for quantitative reasoning. In this chapter, we show how to use probabilistic model checking to verify probabilistic refinement of Event-B models. Such integration allows us to combine logical reasoning about functional correctness with probabilistic reasoning about reliability.


Sign in / Sign up

Export Citation Format

Share Document