Probabilistic model checking of the next-generation airborne collision avoidance system

Author(s):  
Ryan W. Gardner ◽  
Daniel Genin ◽  
Raymond McDowell ◽  
Christopher Rouff ◽  
Anshu Saksena ◽  
...  
Author(s):  
Casey L. Smith ◽  
R. Conrad Rorie ◽  
Kevin J. Monk ◽  
Jillian Keeler ◽  
Garrett G. Sadler

Unmanned aircraft systems (UAS) must comply with specific standards to operate in the National Airspace System (NAS). Among the requirements are the detect and avoid (DAA) capabilities, which include display, alerting, and guidance specifications. Previous studies have queried pilots for their subjective feedback of these display elements on earlier systems; the present study sought pilot evaluations with an initial iteration of the unmanned variant of a Next Generation Airborne Collision Avoidance System (ACAS XU). Sixteen participants piloted simulated aircraft with both standalone and integrated DAA displays. Their opinions were gathered using post-block and post-simulation questionnaires as well as guided debriefs. The data showed pilots had better understanding and comfort with the system when using an integrated display. Pilots also rated ACAS XU alerting and guidance as generally acceptable and effective. Implications for further development of ACAS XU and DAA displays are discussed.


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

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.


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

Sign in / Sign up

Export Citation Format

Share Document