Scholarlink

<p>The present paper describes an <span>Event-B</span> model of the Arrival MANager system (called <span>AMAN</span>), the case study provided by the ABZ’23 conference. The goal of this safety-critical interactive system is to schedule the arrival times of aircraft at airports. This system includes two parts: an autonomous part which predicts the arrival time of an aircraft from external sources (flight plan information, radar and weather information, etc.) and an interface part that permits the Air Traffic Controller (<span>ATCo</span>) to submit requests to <span>AMAN</span>, like changes regarding the arrival times of aircraft. To formally model and verify this critical system, we use a correct-by-construction approach with the <span>Event-B</span> formal method and its refinement process. We mainly consider functional features of the case study; all proof obligations have been discharged using the provers of the <span>Rodin</span> platform under which we carried out our development. To help users understand how <span>AMAN</span> works and its main functionalities, a visualization of the <span>Event-B</span> models was achieved using the <span>VisB</span> component of <span>ProB</span>. Our models have been validated using <span>ProB</span> by checking scenarios related to different functional aspects of the system.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Modeling and verifying an arrival manager using the formal Event-B method

  • 期刊论文

  • 发表日期：

    2025年5月12日

查看全文
  • Amel Mammar,
  • Michael Leuschel

摘要

The present paper describes an Event-B model of the Arrival MANager system (called AMAN), the case study provided by the ABZ’23 conference. The goal of this safety-critical interactive system is to schedule the arrival times of aircraft at airports. This system includes two parts: an autonomous part which predicts the arrival time of an aircraft from external sources (flight plan information, radar and weather information, etc.) and an interface part that permits the Air Traffic Controller (ATCo) to submit requests to AMAN, like changes regarding the arrival times of aircraft. To formally model and verify this critical system, we use a correct-by-construction approach with the Event-B formal method and its refinement process. We mainly consider functional features of the case study; all proof obligations have been discharged using the provers of the Rodin platform under which we carried out our development. To help users understand how AMAN works and its main functionalities, a visualization of the Event-B models was achieved using the VisB component of ProB. Our models have been validated using ProB by checking scenarios related to different functional aspects of the system.