Modeling And Formal Specification Of Air Traffic Control System Using Z Notation
Copyright policy )Modeling And Formal Specification Of Air Traffic Control System Using Z Notation
In this paper, an abstract Air Traffic Control (ATC) System is modeled using Formal Methods, in terms of Z-notation. ATC system is a highly distributed and safety critical system. For modeling of distributed nature of ATC system, a separate queue of flying aircrafts is maintained at each controlled airspace. To ensure safety, it is mandated that each airspace and runway do not exceed its capacity limit in all state operations. Firstly, Requirements Analysis is done using UML diagrams and then the Formal ATC system Model is described by Z-notation. Finally, the Formal ATC system Model is checked and analyzed with Z/EVES tool-set.
Air Traffic Control System, HF5001-6182, Safety Assurance in Complex Systems Development, Set (abstract data type), Advanced Software Engineering, Formal Methods, Model Checking, HB1-3840, Engineering, Air traffic control, Safety properties, FOS: Mathematics, Economic theory. Demography, Business, Safety, Risk, Reliability and Quality, Unified Modeling Language, H1-99, Arithmetic, Formal methods, Computer science, Programming language, Social sciences (General), Aerospace engineering, Computational Theory and Mathematics, Notation, Computer Science, Physical Sciences, Z-notation, Software Reliability Assessment and Prediction, Formal specification, Software, Mathematics, Formal Methods in Software Verification and Control
Air Traffic Control System, HF5001-6182, Safety Assurance in Complex Systems Development, Set (abstract data type), Advanced Software Engineering, Formal Methods, Model Checking, HB1-3840, Engineering, Air traffic control, Safety properties, FOS: Mathematics, Economic theory. Demography, Business, Safety, Risk, Reliability and Quality, Unified Modeling Language, H1-99, Arithmetic, Formal methods, Computer science, Programming language, Social sciences (General), Aerospace engineering, Computational Theory and Mathematics, Notation, Computer Science, Physical Sciences, Z-notation, Software Reliability Assessment and Prediction, Formal specification, Software, Mathematics, Formal Methods in Software Verification and Control
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).2 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!