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 Mondays at the Faculty of Informatics (room depends on the semester, usually B410 or B411), Masaryk University, starting at 10:00. Presentations are usually one hour in length.

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.