Formal Reasoning for Air Traffic Control System Using Event-B Method
| Autor: | Abdessamad Jarrar, Youssef Balouki |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Event b method
Computer science Distributed computing Air traffic management ComputerApplications_COMPUTERSINOTHERSYSTEMS 020206 networking & telecommunications 02 engineering and technology Air traffic control Deadlock Formal reasoning Mathematical proof Formal methods Formalism (philosophy of mathematics) 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing |
| Zdroj: | Computational Science and Its Applications – ICCSA 2018 ISBN: 9783319951645 ICCSA (2) |
| DOI: | 10.1007/978-3-319-95165-2_17 |
| Popis: | We present a formal modeling and verification of Air Traffic Control system (ATC) for airspace management. This system assists air traffic controllers by visualizing aircrafts in the airport vicinity. In such a critical-safety system, the use of robust formal methods that assure bugs absence is highly required. Therefore, we use a formalism of discrete transition systems based on abstraction and refinement along proof obligations. These proofs ensure the consistency of the system by mean of invariants preservation and deadlock freedom. The first guarantee that all invariants hold permanently and thus provide a handy solution for bugs absence verification. The second prove that the system runs forever to avoid deadlock. This modeling and proving enable us to establish that the system is, relatively to some criteria, correct by construction. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|