Publication Information

{'id': 'https://openalex.org/W4391528888', 'doi': 'https://doi.org/10.1109/fit60620.2023.00055', 'title': 'Verification of Safety of Aircraft Arrival Procedure using SPIN Model Checker', 'display_name': 'Verification of Safety of Aircraft Arrival Procedure using SPIN Model Checker', 'publication_year': 2023, 'publication_date': '2023-12-11', 'ids': {'openalex': 'https://openalex.org/W4391528888', 'doi': 'https://doi.org/10.1109/fit60620.2023.00055'}, 'language': 'en', 'primary_location': {'is_oa': False, 'landing_page_url': 'https://doi.org/10.1109/fit60620.2023.00055', 'pdf_url': None, 'source': None, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}, 'type': 'article', 'type_crossref': 'proceedings-article', 'indexed_in': ['crossref'], 'open_access': {'is_oa': False, 'oa_status': 'closed', 'oa_url': None, 'any_repository_has_fulltext': False}, 'authorships': [{'author_position': 'first', 'author': {'id': 'https://openalex.org/A5013719855', 'display_name': 'Muhammad Rashid', 'orcid': 'https://orcid.org/0000-0002-2102-3864'}, 'institutions': [{'id': 'https://openalex.org/I16076960', 'display_name': 'COMSATS University Islamabad', 'ror': 'https://ror.org/00nqqvk19', 'country_code': 'PK', 'type': 'education', 'lineage': ['https://openalex.org/I16076960']}], 'countries': ['PK'], 'is_corresponding': False, 'raw_author_name': 'Muhammad Rashid', 'raw_affiliation_strings': ['Department of Computer Science, COMSATS University Islamabad, Pakistan'], 'affiliations': [{'raw_affiliation_string': 'Department of Computer Science, COMSATS University Islamabad, Pakistan', 'institution_ids': ['https://openalex.org/I16076960']}]}, {'author_position': 'middle', 'author': {'id': 'https://openalex.org/A5030989051', 'display_name': 'Muhammad Qadeer', 'orcid': None}, 'institutions': [{'id': 'https://openalex.org/I16076960', 'display_name': 'COMSATS University Islamabad', 'ror': 'https://ror.org/00nqqvk19', 'country_code': 'PK', 'type': 'education', 'lineage': ['https://openalex.org/I16076960']}], 'countries': ['PK'], 'is_corresponding': False, 'raw_author_name': 'Muhammad Qadeer', 'raw_affiliation_strings': ['Department of Computer Science, COMSATS University Islamabad, Pakistan'], 'affiliations': [{'raw_affiliation_string': 'Department of Computer Science, COMSATS University Islamabad, Pakistan', 'institution_ids': ['https://openalex.org/I16076960']}]}, {'author_position': 'middle', 'author': {'id': 'https://openalex.org/A5054591300', 'display_name': 'Husnain Raza', 'orcid': 'https://orcid.org/0000-0002-2075-5166'}, 'institutions': [{'id': 'https://openalex.org/I16076960', 'display_name': 'COMSATS University Islamabad', 'ror': 'https://ror.org/00nqqvk19', 'country_code': 'PK', 'type': 'education', 'lineage': ['https://openalex.org/I16076960']}], 'countries': ['PK'], 'is_corresponding': False, 'raw_author_name': 'Husnain Raza', 'raw_affiliation_strings': ['Department of Computer Science, COMSATS University Islamabad, Pakistan'], 'affiliations': [{'raw_affiliation_string': 'Department of Computer Science, COMSATS University Islamabad, Pakistan', 'institution_ids': ['https://openalex.org/I16076960']}]}, {'author_position': 'middle', 'author': {'id': 'https://openalex.org/A5068234751', 'display_name': 'M. Rehman', 'orcid': 'https://orcid.org/0000-0002-1069-0637'}, 'institutions': [{'id': 'https://openalex.org/I16076960', 'display_name': 'COMSATS University Islamabad', 'ror': 'https://ror.org/00nqqvk19', 'country_code': 'PK', 'type': 'education', 'lineage': ['https://openalex.org/I16076960']}], 'countries': ['PK'], 'is_corresponding': False, 'raw_author_name': 'Muhammad Masood Ul Rehman', 'raw_affiliation_strings': ['Department of Computer Science, COMSATS University Islamabad, Pakistan'], 'affiliations': [{'raw_affiliation_string': 'Department of Computer Science, COMSATS University Islamabad, Pakistan', 'institution_ids': ['https://openalex.org/I16076960']}]}, {'author_position': 'middle', 'author': {'id': 'https://openalex.org/A5093630782', 'display_name': 'Imran Rasool', 'orcid': None}, 'institutions': [{'id': 'https://openalex.org/I16076960', 'display_name': 'COMSATS University Islamabad', 'ror': 'https://ror.org/00nqqvk19', 'country_code': 'PK', 'type': 'education', 'lineage': ['https://openalex.org/I16076960']}], 'countries': ['PK'], 'is_corresponding': False, 'raw_author_name': 'Imran Rasool', 'raw_affiliation_strings': ['Department of Computer Science, COMSATS University Islamabad, Pakistan'], 'affiliations': [{'raw_affiliation_string': 'Department of Computer Science, COMSATS University Islamabad, Pakistan', 'institution_ids': ['https://openalex.org/I16076960']}]}, {'author_position': 'last', 'author': {'id': 'https://openalex.org/A5022909686', 'display_name': 'Nazir Ahmad Zafar', 'orcid': 'https://orcid.org/0000-0003-1679-6851'}, 'institutions': [{'id': 'https://openalex.org/I16076960', 'display_name': 'COMSATS University Islamabad', 'ror': 'https://ror.org/00nqqvk19', 'country_code': 'PK', 'type': 'education', 'lineage': ['https://openalex.org/I16076960']}], 'countries': ['PK'], 'is_corresponding': False, 'raw_author_name': 'Nazir Ahmad Zafar', 'raw_affiliation_strings': ['Department of Computer Science, COMSATS University Islamabad, Pakistan'], 'affiliations': [{'raw_affiliation_string': 'Department of Computer Science, COMSATS University Islamabad, Pakistan', 'institution_ids': ['https://openalex.org/I16076960']}]}], 'institution_assertions': [], 'countries_distinct_count': 1, 'institutions_distinct_count': 1, 'corresponding_author_ids': [], 'corresponding_institution_ids': [], 'apc_list': None, 'apc_paid': None, 'fwci': 0.0, 'has_fulltext': False, 'cited_by_count': 0, 'citation_normalized_percentile': {'value': 0.0, 'is_in_top_1_percent': False, 'is_in_top_10_percent': False}, 'cited_by_percentile_year': {'min': 0, 'max': 68}, 'biblio': {'volume': None, 'issue': None, 'first_page': '262', 'last_page': '267'}, 'is_retracted': False, 'is_paratext': False, 'primary_topic': {'id': 'https://openalex.org/T10142', 'display_name': 'Formal Methods in Verification', 'score': 0.9994, 'subfield': {'id': 'https://openalex.org/subfields/1703', 'display_name': 'Computational Theory and Mathematics'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, 'topics': [{'id': 'https://openalex.org/T10142', 'display_name': 'Formal Methods in Verification', 'score': 0.9994, 'subfield': {'id': 'https://openalex.org/subfields/1703', 'display_name': 'Computational Theory and Mathematics'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, {'id': 'https://openalex.org/T10933', 'display_name': 'Real-Time Systems Scheduling', 'score': 0.9957, 'subfield': {'id': 'https://openalex.org/subfields/1708', 'display_name': 'Hardware and Architecture'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, {'id': 'https://openalex.org/T10743', 'display_name': 'Software Testing and Debugging Techniques', 'score': 0.995, 'subfield': {'id': 'https://openalex.org/subfields/1712', 'display_name': 'Software'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}], 'keywords': [{'id': 'https://openalex.org/keywords/life-critical-system', 'display_name': 'Life-critical system', 'score': 0.4527923}, {'id': 'https://openalex.org/keywords/system-safety', 'display_name': 'System safety', 'score': 0.43726492}, {'id': 'https://openalex.org/keywords/critical-system', 'display_name': 'Critical system', 'score': 0.41616464}], 'concepts': [{'id': 'https://openalex.org/C55439883', 'wikidata': 'https://www.wikidata.org/wiki/Q360812', 'display_name': 'Correctness', 'level': 2, 'score': 0.94030416}, {'id': 'https://openalex.org/C110251889', 'wikidata': 'https://www.wikidata.org/wiki/Q1569697', 'display_name': 'Model checking', 'level': 2, 'score': 0.8430886}, {'id': 'https://openalex.org/C41008148', 'wikidata': 'https://www.wikidata.org/wiki/Q21198', 'display_name': 'Computer science', 'level': 0, 'score': 0.7205054}, {'id': 'https://openalex.org/C4777664', 'wikidata': 'https://www.wikidata.org/wiki/Q1536492', 'display_name': 'Linear temporal logic', 'level': 2, 'score': 0.59130937}, {'id': 'https://openalex.org/C111498074', 'wikidata': 'https://www.wikidata.org/wiki/Q173326', 'display_name': 'Formal verification', 'level': 2, 'score': 0.4790548}, {'id': 'https://openalex.org/C25016198', 'wikidata': 'https://www.wikidata.org/wiki/Q781833', 'display_name': 'Temporal logic', 'level': 2, 'score': 0.45556286}, {'id': 'https://openalex.org/C163707989', 'wikidata': 'https://www.wikidata.org/wiki/Q1996307', 'display_name': 'Life-critical system', 'level': 3, 'score': 0.4527923}, {'id': 'https://openalex.org/C132525143', 'wikidata': 'https://www.wikidata.org/wiki/Q141488', 'display_name': 'Graph', 'level': 2, 'score': 0.44554085}, {'id': 'https://openalex.org/C132835097', 'wikidata': 'https://www.wikidata.org/wiki/Q7663745', 'display_name': 'System safety', 'level': 2, 'score': 0.43726492}, {'id': 'https://openalex.org/C2780074322', 'wikidata': 'https://www.wikidata.org/wiki/Q28130043', 'display_name': 'Critical system', 'level': 2, 'score': 0.41616464}, {'id': 'https://openalex.org/C200601418', 'wikidata': 'https://www.wikidata.org/wiki/Q2193887', 'display_name': 'Reliability engineering', 'level': 1, 'score': 0.3148229}, {'id': 'https://openalex.org/C80444323', 'wikidata': 'https://www.wikidata.org/wiki/Q2878974', 'display_name': 'Theoretical computer science', 'level': 1, 'score': 0.2887483}, {'id': 'https://openalex.org/C11413529', 'wikidata': 'https://www.wikidata.org/wiki/Q8366', 'display_name': 'Algorithm', 'level': 1, 'score': 0.26269498}, {'id': 'https://openalex.org/C199360897', 'wikidata': 'https://www.wikidata.org/wiki/Q9143', 'display_name': 'Programming language', 'level': 1, 'score': 0.25071317}, {'id': 'https://openalex.org/C115903868', 'wikidata': 'https://www.wikidata.org/wiki/Q80993', 'display_name': 'Software engineering', 'level': 1, 'score': 0.11401373}, {'id': 'https://openalex.org/C127413603', 'wikidata': 'https://www.wikidata.org/wiki/Q11023', 'display_name': 'Engineering', 'level': 0, 'score': 0.10617408}, {'id': 'https://openalex.org/C2777904410', 'wikidata': 'https://www.wikidata.org/wiki/Q7397', 'display_name': 'Software', 'level': 2, 'score': 0.0}], 'mesh': [], 'locations_count': 1, 'locations': [{'is_oa': False, 'landing_page_url': 'https://doi.org/10.1109/fit60620.2023.00055', 'pdf_url': None, 'source': None, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}], 'best_oa_location': None, 'sustainable_development_goals': [], 'grants': [], 'datasets': [], 'versions': [], 'referenced_works_count': 25, 'referenced_works': ['https://openalex.org/W1971475149', 'https://openalex.org/W1977223654', 'https://openalex.org/W2118555022', 'https://openalex.org/W2533805347', 'https://openalex.org/W2798895321', 'https://openalex.org/W2905280642', 'https://openalex.org/W2950836712', 'https://openalex.org/W2951308394', 'https://openalex.org/W2966102633', 'https://openalex.org/W2972405155', 'https://openalex.org/W2980890518', 'https://openalex.org/W2995068468', 'https://openalex.org/W3003742662', 'https://openalex.org/W3005782417', 'https://openalex.org/W3105943227', 'https://openalex.org/W3112216475', 'https://openalex.org/W3115763602', 'https://openalex.org/W3157737336', 'https://openalex.org/W3166996443', 'https://openalex.org/W3210090433', 'https://openalex.org/W4287888022', 'https://openalex.org/W4312435721', 'https://openalex.org/W4318576775', 'https://openalex.org/W4361858704', 'https://openalex.org/W4376605471'], 'related_works': ['https://openalex.org/W3021103820', 'https://openalex.org/W2995934072', 'https://openalex.org/W2905170665', 'https://openalex.org/W2891366153', 'https://openalex.org/W2763487042', 'https://openalex.org/W2389909316', 'https://openalex.org/W2352594534', 'https://openalex.org/W2184478364', 'https://openalex.org/W2151392245', 'https://openalex.org/W2124110813'], 'abstract_inverted_index': {'The': [0], 'volume': [1], 'of': [2, 19, 25, 32, 38, 56, 68, 148, 190], 'air': [3, 9], 'traffic': [4, 10], 'increases': [5], 'dramatically': [6], 'and': [7, 29, 66, 122, 156, 161, 173], 'the': [8, 20, 36, 54, 57, 64, 69, 102, 112, 120, 124, 128, 134, 146, 150, 179], 'control': [11], 'system': [12, 21, 41, 121, 165], 'is': [13, 42, 140, 176, 185], 'a': [14, 40, 116], 'safety': [15, 37, 65, 109, 129, 191], 'critical': [16, 192], 'system.': [17, 58, 113, 135], 'Failure': [18], 'can': [22, 49], 'cause': [23], 'loss': [24], 'human': [26], 'life,': [27], 'cost,': [28], 'hard': [30], 'work': [31], 'many': [33], 'people.': [34], 'Therefore,': [35], 'such': [39], 'necessary': [43], 'to': [44, 63, 76, 83, 142, 187], 'prevent': [45], 'these': [46], 'losses.': [47], 'Safety': [48], 'be': [50], 'ensured': [51], 'by': [52, 106], 'checking': [53, 107], 'correctness': [55, 67, 189], 'We': [59, 114], 'address': [60], 'problems': [61], 'related': [62, 75], 'aircraft': [70, 77, 103], 'arrival': [71, 78, 104], 'procedure.': [72], 'Research': [73], 'exists': [74], 'procedure': [79, 105], 'analysis': [80, 175], 'but': [81], 'according': [82], 'our': [84, 164], 'knowledge,': [85], 'we': [86, 100, 131], 'do': [87], 'not': [88], 'find': [89], 'its': [90], 'formal': [91], 'verification': [92], 'in': [93, 145], 'SPIN': [94, 180], 'model': [95, 151, 181], 'checker.': [96, 182], 'In': [97], 'this': [98], 'paper,': [99], 'verify': [101], 'specific': [108], 'properties': [110, 130, 144], 'on': [111, 133], 'generate': [115], 'program': [117, 154], 'graph': [118, 155], 'for': [119, 127], 'give': [123], 'LTL': [125, 157, 168], 'formula': [126, 158, 169], 'define': [132], 'Linear': [136], 'temporal': [137], 'logic': [138], '(LTL)': [139], 'used': [141], 'specify': [143], 'form': [147], 'formulas.': [149], 'checker': [152], 'takes': [153], 'as': [159], 'input': [160], 'check': [162], 'whether': [163], 'satisfied': [166], 'with': [167], 'or': [170], 'not.': [171], 'Verification': [172], 'result': [174], 'done': [177], 'using': [178], 'This': [183], 'research': [184], 'beneficial': [186], 'ensure': [188], 'systems.': [193]}, 'cited_by_api_url': 'https://api.openalex.org/works?filter=cites:W4391528888', 'counts_by_year': [], 'updated_date': '2024-12-16T01:13:46.676533', 'created_date': '2024-02-06'}