ParaDiSe Seminar
The ParaDiSe Seminar is a working forum for the presentation of ongoing and finished research in the areas related to the specification, modelling, analysis, and verification of software systems.
The meetings are held on Thursday at the Faculty of Informatics, Masaryk University, starting at 12:00.
Seminar Programme — Spring 2008
Modeling and Verification of Air Traffic Managment Systems
Air Traffic Managment (ATM), consisting of many complex and life critical sub-systems, is used world-wide to control the air transportation. The general scheme of the current ATM exhibits flaws of its centralized design meaning that the system is not about to scale beyond a certain volume of air traffic. Unfortunately, the amount of air transportation is continosly growing. As a result new scheme of ATM is expected to be designed and implemented in a few upcomming years. Due to the life-critical nature of ATM, it is inevitable that formal modeling and verification of the new scheme will take a significant role during its design and validation.
The aim of the seminar in this semester is to explore existing techniques used and approaches taken to model, simulate or verify (parts) of current ATM systems.
- February 25, 2008
Fundamentals of Air Traffic Control (slides)
(Luboš Brim) - March 3, 2008
Modeling and Verification of an Air Traffic Concept of Operations (slides)
(Sven Dražan / Pavel Šimeček) - March 10, 2008
Application of design for Verification with Concurrency Controllers to Air Traffic Control Software (slides)
(Ondřej Kuzník / Barbora Zimmerová) - March 17, 2008
Formal verification of the NASA runway safety monitor (slides)
(Tomáš Janoušek / Pavlína Vařeková) - March 24, 2008
Cancelled -- Easter Holidays
- March 31, 2008
Cancelled -- ETAPS
- April 7, 2008
Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm (slides)
(Jitka Kudrnáčová / Jakub Chaloupka) - April 14, 2008
Formal Verification of Human-Automation Interaction (slides)
(Jan Krčál / Barbora Zimmerova) - April 21, 2008
On the Formal Verification of Conflict Detection Algorithms (slides)
(Jana Fabriková / Nikola Beneš) - April 28, 2008
Verification of An Air-Traffic Control System with Probabilistic Real-time Model-checking (slides)
(Jana Tůmová / Jakub Chaloupka) - May 5, 2008
Verifying Time Partitioning in the DEOS Scheduling Kernel (slides)
(Petr Ročkai / Pavlína Vařeková) - May 12, 2008
Technologies of Distributed Simulation (DIS, HLA)
Petr Gotthard (Honeywell)Abstract: Introduction to distributed simulation and its technologies. Distributed Interactive Simulation (DIS). High Level Architecture (HLA).