Requirements Analysis of Air Traffic Control System Using Formal Methods

Formal methods is an emerging technology that uses mathematical notations to write precise and unambiguous specifications which makes it possible to prove and analyze certain properties of the system so that errors and inconsistencies are identified during early stages of the development process. In...

Full description

Saved in:
Bibliographic Details
Main Authors: Jamal, M., Zafar, N.A.
Format: Conference Proceeding
Language:English
Subjects:
Air safety
Air traffic control
Aircraft
Computer errors
Computer science
Error correction
Graph theory
Humans
Information analysis
Network topology
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by
cites
container_end_page 7
container_issue
container_start_page 1
container_title
container_volume
creator Jamal, M.
Zafar, N.A.
description Formal methods is an emerging technology that uses mathematical notations to write precise and unambiguous specifications which makes it possible to prove and analyze certain properties of the system so that errors and inconsistencies are identified during early stages of the development process. In this paper formal methods in terms of Z notation is applied for the specification of safety critical system of Air Traffic Control (ATC). Firstly, ATC system model in real world is described. For connectivity of different zones of airspace, the real world ATC system is transformed into a directed graph, which is then used to formalize the major components of formal ATC Model i.e static Topology, Network State, Aircraft and Controller. The whole Formal ATC Model is then presented as encapsulation of formal models of its basic components. Finally, the Formal A TC system Model is checked and analyzed with Z/EVES tool-set.
doi_str_mv 10.1109/ICIET.2007.4381340
format conference_proceeding
fullrecord <record><control><sourceid>ieee_6IE</sourceid><recordid>TN_cdi_ieee_primary_4381340</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><ieee_id>4381340</ieee_id><sourcerecordid>4381340</sourcerecordid><originalsourceid>FETCH-LOGICAL-i90t-b216b1b7261e2ca180f5bb3aee31f4b138e5c711213fb7ddae65c905ea7321063</originalsourceid><addsrcrecordid>eNpVj8tKxDAUQCMiKGN_QDf5gdZ7k7Rpl6XMOIURQet6SNobjfShSV3M37twNq4OZ3PgMHaHkCFC9dA27bbLBIDOlCxRKrhgSaVLVEIpFErj5T8v1DVLYvwEANSFQihv2P6Fvn98oInmNfJ6NuMp-sgXx2sfeBeMc77nzTKvYRn56ymuNPG36Od3vlvCZEb-ROvHMsRbduXMGCk5c8O63bZr9unh-bFt6kPqK1hTK7CwaLUokERvsASXWysNkUSnLMqS8l4jCpTO6mEwVOR9BTkZLQVCITfs_i_riej4Ffxkwul43pe_EtRNrQ</addsrcrecordid><sourcetype>Publisher</sourcetype><iscdi>true</iscdi><recordtype>conference_proceeding</recordtype></control><display><type>conference_proceeding</type><title>Requirements Analysis of Air Traffic Control System Using Formal Methods</title><source>IEEE Electronic Library (IEL) Conference Proceedings</source><creator>Jamal, M. ; Zafar, N.A.</creator><creatorcontrib>Jamal, M. ; Zafar, N.A.</creatorcontrib><description>Formal methods is an emerging technology that uses mathematical notations to write precise and unambiguous specifications which makes it possible to prove and analyze certain properties of the system so that errors and inconsistencies are identified during early stages of the development process. In this paper formal methods in terms of Z notation is applied for the specification of safety critical system of Air Traffic Control (ATC). Firstly, ATC system model in real world is described. For connectivity of different zones of airspace, the real world ATC system is transformed into a directed graph, which is then used to formalize the major components of formal ATC Model i.e static Topology, Network State, Aircraft and Controller. The whole Formal ATC Model is then presented as encapsulation of formal models of its basic components. Finally, the Formal A TC system Model is checked and analyzed with Z/EVES tool-set.</description><identifier>ISBN: 9781424412464</identifier><identifier>ISBN: 1424412463</identifier><identifier>EISBN: 9781424412471</identifier><identifier>EISBN: 1424412471</identifier><identifier>DOI: 10.1109/ICIET.2007.4381340</identifier><language>eng</language><publisher>IEEE</publisher><subject>Air safety ; Air traffic control ; Aircraft ; Computer errors ; Computer science ; Error correction ; Graph theory ; Humans ; Information analysis ; Network topology</subject><ispartof>2007 International Conference on Information and Emerging Technologies, 2007, p.1-7</ispartof><woscitedreferencessubscribed>false</woscitedreferencessubscribed></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><linktohtml>$$Uhttps://ieeexplore.ieee.org/document/4381340$$EHTML$$P50$$Gieee$$H</linktohtml><link.rule.ids>309,310,777,781,786,787,2052,27906,54901</link.rule.ids><linktorsrc>$$Uhttps://ieeexplore.ieee.org/document/4381340$$EView_record_in_IEEE$$FView_record_in_$$GIEEE</linktorsrc></links><search><creatorcontrib>Jamal, M.</creatorcontrib><creatorcontrib>Zafar, N.A.</creatorcontrib><title>Requirements Analysis of Air Traffic Control System Using Formal Methods</title><title>2007 International Conference on Information and Emerging Technologies</title><addtitle>ICIET</addtitle><description>Formal methods is an emerging technology that uses mathematical notations to write precise and unambiguous specifications which makes it possible to prove and analyze certain properties of the system so that errors and inconsistencies are identified during early stages of the development process. In this paper formal methods in terms of Z notation is applied for the specification of safety critical system of Air Traffic Control (ATC). Firstly, ATC system model in real world is described. For connectivity of different zones of airspace, the real world ATC system is transformed into a directed graph, which is then used to formalize the major components of formal ATC Model i.e static Topology, Network State, Aircraft and Controller. The whole Formal ATC Model is then presented as encapsulation of formal models of its basic components. Finally, the Formal A TC system Model is checked and analyzed with Z/EVES tool-set.</description><subject>Air safety</subject><subject>Air traffic control</subject><subject>Aircraft</subject><subject>Computer errors</subject><subject>Computer science</subject><subject>Error correction</subject><subject>Graph theory</subject><subject>Humans</subject><subject>Information analysis</subject><subject>Network topology</subject><isbn>9781424412464</isbn><isbn>1424412463</isbn><isbn>9781424412471</isbn><isbn>1424412471</isbn><fulltext>true</fulltext><rsrctype>conference_proceeding</rsrctype><creationdate>2007</creationdate><recordtype>conference_proceeding</recordtype><sourceid>6IE</sourceid><recordid>eNpVj8tKxDAUQCMiKGN_QDf5gdZ7k7Rpl6XMOIURQet6SNobjfShSV3M37twNq4OZ3PgMHaHkCFC9dA27bbLBIDOlCxRKrhgSaVLVEIpFErj5T8v1DVLYvwEANSFQihv2P6Fvn98oInmNfJ6NuMp-sgXx2sfeBeMc77nzTKvYRn56ymuNPG36Od3vlvCZEb-ROvHMsRbduXMGCk5c8O63bZr9unh-bFt6kPqK1hTK7CwaLUokERvsASXWysNkUSnLMqS8l4jCpTO6mEwVOR9BTkZLQVCITfs_i_riej4Ffxkwul43pe_EtRNrQ</recordid><startdate>200707</startdate><enddate>200707</enddate><creator>Jamal, M.</creator><creator>Zafar, N.A.</creator><general>IEEE</general><scope>6IE</scope><scope>6IL</scope><scope>CBEJK</scope><scope>RIE</scope><scope>RIL</scope></search><sort><creationdate>200707</creationdate><title>Requirements Analysis of Air Traffic Control System Using Formal Methods</title><author>Jamal, M. ; Zafar, N.A.</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-i90t-b216b1b7261e2ca180f5bb3aee31f4b138e5c711213fb7ddae65c905ea7321063</frbrgroupid><rsrctype>conference_proceedings</rsrctype><prefilter>conference_proceedings</prefilter><language>eng</language><creationdate>2007</creationdate><topic>Air safety</topic><topic>Air traffic control</topic><topic>Aircraft</topic><topic>Computer errors</topic><topic>Computer science</topic><topic>Error correction</topic><topic>Graph theory</topic><topic>Humans</topic><topic>Information analysis</topic><topic>Network topology</topic><toplevel>online_resources</toplevel><creatorcontrib>Jamal, M.</creatorcontrib><creatorcontrib>Zafar, N.A.</creatorcontrib><collection>IEEE Electronic Library (IEL) Conference Proceedings</collection><collection>IEEE Proceedings Order Plan All Online (POP All Online) 1998-present by volume</collection><collection>IEEE Xplore All Conference Proceedings</collection><collection>IEEE Xplore</collection><collection>IEEE Proceedings Order Plans (POP All) 1998-Present</collection></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext_linktorsrc</fulltext></delivery><addata><au>Jamal, M.</au><au>Zafar, N.A.</au><format>book</format><genre>proceeding</genre><ristype>CONF</ristype><atitle>Requirements Analysis of Air Traffic Control System Using Formal Methods</atitle><btitle>2007 International Conference on Information and Emerging Technologies</btitle><stitle>ICIET</stitle><date>2007-07</date><risdate>2007</risdate><spage>1</spage><epage>7</epage><pages>1-7</pages><isbn>9781424412464</isbn><isbn>1424412463</isbn><eisbn>9781424412471</eisbn><eisbn>1424412471</eisbn><abstract>Formal methods is an emerging technology that uses mathematical notations to write precise and unambiguous specifications which makes it possible to prove and analyze certain properties of the system so that errors and inconsistencies are identified during early stages of the development process. In this paper formal methods in terms of Z notation is applied for the specification of safety critical system of Air Traffic Control (ATC). Firstly, ATC system model in real world is described. For connectivity of different zones of airspace, the real world ATC system is transformed into a directed graph, which is then used to formalize the major components of formal ATC Model i.e static Topology, Network State, Aircraft and Controller. The whole Formal ATC Model is then presented as encapsulation of formal models of its basic components. Finally, the Formal A TC system Model is checked and analyzed with Z/EVES tool-set.</abstract><pub>IEEE</pub><doi>10.1109/ICIET.2007.4381340</doi><tpages>7</tpages></addata></record>
fulltext fulltext_linktorsrc
identifier ISBN: 9781424412464
ispartof 2007 International Conference on Information and Emerging Technologies, 2007, p.1-7
issn
language eng
recordid cdi_ieee_primary_4381340
source IEEE Electronic Library (IEL) Conference Proceedings
subjects Air safety
Air traffic control
Aircraft
Computer errors
Computer science
Error correction
Graph theory
Humans
Information analysis
Network topology
title Requirements Analysis of Air Traffic Control System Using Formal Methods
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2025-01-20T05%3A35%3A56IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-ieee_6IE&rft_val_fmt=info:ofi/fmt:kev:mtx:book&rft.genre=proceeding&rft.atitle=Requirements%20Analysis%20of%20Air%20Traffic%20Control%20System%20Using%20Formal%20Methods&rft.btitle=2007%20International%20Conference%20on%20Information%20and%20Emerging%20Technologies&rft.au=Jamal,%20M.&rft.date=2007-07&rft.spage=1&rft.epage=7&rft.pages=1-7&rft.isbn=9781424412464&rft.isbn_list=1424412463&rft_id=info:doi/10.1109/ICIET.2007.4381340&rft.eisbn=9781424412471&rft.eisbn_list=1424412471&rft_dat=%3Cieee_6IE%3E4381340%3C/ieee_6IE%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-i90t-b216b1b7261e2ca180f5bb3aee31f4b138e5c711213fb7ddae65c905ea7321063%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rft_ieee_id=4381340&rfr_iscdi=true