Publication Information

{'id': 'https://openalex.org/W4390481443', 'doi': 'https://doi.org/10.1109/icet59753.2023.10374485', 'title': 'Formal Verification of Aircraft Departure Procedure Using Spin Model Checker', 'display_name': 'Formal Verification of Aircraft Departure Procedure Using Spin Model Checker', 'publication_year': 2023, 'publication_date': '2023-11-06', 'ids': {'openalex': 'https://openalex.org/W4390481443', 'doi': 'https://doi.org/10.1109/icet59753.2023.10374485'}, 'language': 'en', 'primary_location': {'is_oa': False, 'landing_page_url': 'https://doi.org/10.1109/icet59753.2023.10374485', '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/A5104222837', 'display_name': 'Muhammad Rashid', '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 Rashid', 'raw_affiliation_strings': ['Dept of Computer Science, COMSATS University Islamabad, Pakistan'], 'affiliations': [{'raw_affiliation_string': 'Dept 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': ['Dept of Computer Science, COMSATS University Islamabad, Pakistan'], 'affiliations': [{'raw_affiliation_string': 'Dept 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': ['Dept of Computer Science, COMSATS University Islamabad, Pakistan'], 'affiliations': [{'raw_affiliation_string': 'Dept 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': ['Dept of Computer Science, COMSATS University Islamabad, Pakistan'], 'affiliations': [{'raw_affiliation_string': 'Dept of Computer Science, COMSATS University Islamabad, Pakistan', 'institution_ids': ['https://openalex.org/I16076960']}]}, {'author_position': 'middle', 'author': {'id': 'https://openalex.org/A5093630793', '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': ['Dept of Computer Science, COMSATS University Islamabad, Pakistan'], 'affiliations': [{'raw_affiliation_string': 'Dept 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': ['Dept of Computer Science, COMSATS University Islamabad, Pakistan'], 'affiliations': [{'raw_affiliation_string': 'Dept 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': '165', 'last_page': '170'}, 'is_retracted': False, 'is_paratext': False, 'primary_topic': {'id': 'https://openalex.org/T10743', 'display_name': 'Software Testing and Debugging Techniques', 'score': 0.9985, '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'}}, 'topics': [{'id': 'https://openalex.org/T10743', 'display_name': 'Software Testing and Debugging Techniques', 'score': 0.9985, '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'}}, {'id': 'https://openalex.org/T10142', 'display_name': 'Formal Methods in Verification', 'score': 0.9985, '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/T13295', 'display_name': 'Safety Systems Engineering in Autonomy', 'score': 0.9925, 'subfield': {'id': 'https://openalex.org/subfields/2213', 'display_name': 'Safety, Risk, Reliability and Quality'}, 'field': {'id': 'https://openalex.org/fields/22', 'display_name': 'Engineering'}, '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.518454}], 'concepts': [{'id': 'https://openalex.org/C55439883', 'wikidata': 'https://www.wikidata.org/wiki/Q360812', 'display_name': 'Correctness', 'level': 2, 'score': 0.9360338}, {'id': 'https://openalex.org/C110251889', 'wikidata': 'https://www.wikidata.org/wiki/Q1569697', 'display_name': 'Model checking', 'level': 2, 'score': 0.86747265}, {'id': 'https://openalex.org/C41008148', 'wikidata': 'https://www.wikidata.org/wiki/Q21198', 'display_name': 'Computer science', 'level': 0, 'score': 0.69708717}, {'id': 'https://openalex.org/C4777664', 'wikidata': 'https://www.wikidata.org/wiki/Q1536492', 'display_name': 'Linear temporal logic', 'level': 2, 'score': 0.5828166}, {'id': 'https://openalex.org/C111498074', 'wikidata': 'https://www.wikidata.org/wiki/Q173326', 'display_name': 'Formal verification', 'level': 2, 'score': 0.5801769}, {'id': 'https://openalex.org/C163707989', 'wikidata': 'https://www.wikidata.org/wiki/Q1996307', 'display_name': 'Life-critical system', 'level': 3, 'score': 0.518454}, {'id': 'https://openalex.org/C132525143', 'wikidata': 'https://www.wikidata.org/wiki/Q141488', 'display_name': 'Graph', 'level': 2, 'score': 0.43015623}, {'id': 'https://openalex.org/C200601418', 'wikidata': 'https://www.wikidata.org/wiki/Q2193887', 'display_name': 'Reliability engineering', 'level': 1, 'score': 0.33453023}, {'id': 'https://openalex.org/C80444323', 'wikidata': 'https://www.wikidata.org/wiki/Q2878974', 'display_name': 'Theoretical computer science', 'level': 1, 'score': 0.27043283}, {'id': 'https://openalex.org/C199360897', 'wikidata': 'https://www.wikidata.org/wiki/Q9143', 'display_name': 'Programming language', 'level': 1, 'score': 0.26598904}, {'id': 'https://openalex.org/C127413603', 'wikidata': 'https://www.wikidata.org/wiki/Q11023', 'display_name': 'Engineering', 'level': 0, 'score': 0.115278274}, {'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/icet59753.2023.10374485', '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': 37, 'referenced_works': ['https://openalex.org/W1954107640', 'https://openalex.org/W1971475149', 'https://openalex.org/W1977223654', 'https://openalex.org/W2118555022', 'https://openalex.org/W2329992836', 'https://openalex.org/W2339136178', 'https://openalex.org/W2482974097', 'https://openalex.org/W2533805347', 'https://openalex.org/W2611228172', '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/W3044882843', 'https://openalex.org/W3094665111', 'https://openalex.org/W3098181561', 'https://openalex.org/W3112216475', 'https://openalex.org/W3115763602', 'https://openalex.org/W3157737336', 'https://openalex.org/W3159305744', 'https://openalex.org/W3166996443', 'https://openalex.org/W3210090433', 'https://openalex.org/W4212850236', 'https://openalex.org/W4287888022', 'https://openalex.org/W4312435721', 'https://openalex.org/W4318576775', 'https://openalex.org/W4321019928', 'https://openalex.org/W4361858704', 'https://openalex.org/W4376605471', 'https://openalex.org/W4378714752', 'https://openalex.org/W4379781097'], 'related_works': ['https://openalex.org/W70902631', 'https://openalex.org/W4391528888', 'https://openalex.org/W4390481443', 'https://openalex.org/W3097218026', 'https://openalex.org/W2350953867', 'https://openalex.org/W2127730763', 'https://openalex.org/W2111870610', 'https://openalex.org/W2093227835', 'https://openalex.org/W2085847302', 'https://openalex.org/W1592102986'], 'abstract_inverted_index': {'The': [0], 'volume': [1], 'of': [2, 9, 21, 26, 33, 38, 54, 66, 143, 183], 'air': [3, 10], 'traffic': [4, 11], 'increase': [5], 'dramatically': [6], 'and': [7, 30, 64, 119, 150, 155, 167], 'safety': [8, 37, 63, 108, 124, 184], 'systems': [12], 'are': [13], 'becoming': [14], 'critical': [15, 185], 'issue': [16], 'day': [17], 'by': [18, 51, 105], 'day.': [19], 'Failure': [20], 'system': [22, 40, 118, 159], 'can': [23, 48], 'cause': [24], 'loss': [25], 'human': [27], 'life,': [28], 'cost': [29], 'hard': [31], 'work': [32], 'many': [34], 'peoples.': [35], 'Therefore,': [36], 'such': [39], 'is': [41, 135, 170, 178], 'necessary': [42], 'to': [43, 61, 76, 83, 137, 180], 'prevent': [44], 'these': [45], 'loses.': [46], 'Safety': [47], 'be': [49], 'ensured': [50], 'checking': [52, 106], 'correctness': [53, 65, 182], 'the': [55, 67, 111, 129, 141], 'system.': [56, 112, 130], 'We': [57, 113], 'address': [58], 'problem': [59], 'related': [60, 75], 'ensuring': [62], 'aircraft': [68, 77, 102], 'departure': [69, 78, 103], 'procedure': [70, 79, 104], 'using': [71, 172], 'SPIN.': [72], 'Research': [73], 'exists': [74], 'analysis': [80, 169], 'but': [81], 'according': [82], 'our': [84, 158], 'knowledge': [85], 'we': [86, 100, 126], 'do': [87], 'not': [88], 'find': [89], 'its': [90], 'formal': [91], 'verification': [92], 'in': [93, 140], 'SPIN': [94, 173], 'model': [95, 174], 'checker.': [96, 175], 'In': [97], 'this': [98], 'paper,': [99], 'verify': [101], 'specific': [107], 'properties': [109, 125, 139], 'on': [110, 128], 'generate': [114], 'program': [115, 148], 'graph': [116, 149], 'for': [117, 123], 'give': [120], 'LTL': [121, 151, 162], 'formula': [122, 152, 163], 'define': [127], 'Linear': [131], 'temprol': [132], 'logic': [133], '(LTL)': [134], 'use': [136], 'specify': [138], 'form': [142], 'formula.': [144], 'Model': [145], 'checker': [146], 'take': [147], 'as': [153], 'input': [154], 'check': [156], 'whether': [157], 'satisfied': [160], 'with': [161], 'or': [164], 'not.': [165], 'Verification': [166], 'result': [168], 'done': [171], 'This': [176], 'research': [177], 'beneficial': [179], 'ensure': [181], 'systems.': [186]}, 'cited_by_api_url': 'https://api.openalex.org/works?filter=cites:W4390481443', 'counts_by_year': [], 'updated_date': '2024-12-12T20:18:54.329502', 'created_date': '2024-01-02'}