A check-points extraction method for formal verification

Name: Work Video:
Duration: 3 min 30 s
Description: In design of complex and large scale systems, formal verification has played an important role. However, it is inefficiency to verify the entire systems. This article considers the case where designers of systems can extract check-points easily in formal verification. Moreover, we propose a method by which temporal formulas can be obtained inductively for specifications in formal verification.
Chikatoshi Yamada; Yasunori Nagata
{'id': 'https://openalex.org/W161255303', 'doi': None, 'title': 'A check-points extraction method for formal verification', 'display_name': 'A check-points extraction method for formal verification', 'publication_year': 2007, 'publication_date': '2007-08-24', 'ids': {'openalex': 'https://openalex.org/W161255303', 'mag': '161255303'}, 'language': 'en', 'primary_location': {'is_oa': False, 'landing_page_url': 'https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.413.323&rep=rep1&type=pdf', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S4306419863', 'display_name': 'International Conference on Systems', 'issn_l': None, 'issn': None, 'is_oa': False, 'is_in_doaj': False, 'is_core': False, 'host_organization': None, 'host_organization_name': None, 'host_organization_lineage': [], 'host_organization_lineage_names': [], 'type': 'conference'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}, 'type': 'article', 'type_crossref': 'proceedings-article', 'indexed_in': [], '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/A5050809285', 'display_name': 'Chikatoshi Yamada', 'orcid': None}, 'institutions': [{'id': 'https://openalex.org/I4210126936', 'display_name': 'National Institute of Technology Okinawa College', 'ror': 'https://ror.org/02q9dpj81', 'country_code': 'JP', 'type': 'education', 'lineage': ['https://openalex.org/I4210120810', 'https://openalex.org/I4210126936']}], 'countries': ['JP'], 'is_corresponding': False, 'raw_author_name': 'Chikatoshi Yamada', 'raw_affiliation_strings': ['Okinawa National College of Tech., Dept. of Inf. Comm. Syst. Eng., Okinawa, Japan#TAB#'], 'affiliations': [{'raw_affiliation_string': 'Okinawa National College of Tech., Dept. of Inf. Comm. Syst. Eng., Okinawa, Japan#TAB#', 'institution_ids': ['https://openalex.org/I4210126936']}]}, {'author_position': 'last', 'author': {'id': 'https://openalex.org/A5072873584', 'display_name': 'Yasunori Nagata', 'orcid': 'https://orcid.org/0000-0001-5895-8826'}, 'institutions': [{'id': 'https://openalex.org/I32915989', 'display_name': 'University of the Ryukyus', 'ror': 'https://ror.org/02z1n9q24', 'country_code': 'JP', 'type': 'education', 'lineage': ['https://openalex.org/I32915989']}], 'countries': ['JP'], 'is_corresponding': False, 'raw_author_name': 'Yasunori Nagata', 'raw_affiliation_strings': ['Univ. of the Ryukyus, Dept. of Electrical & Electronics Eng., Okinawa, Japan'], 'affiliations': [{'raw_affiliation_string': 'Univ. of the Ryukyus, Dept. of Electrical & Electronics Eng., Okinawa, Japan', 'institution_ids': ['https://openalex.org/I32915989']}]}], 'institution_assertions': [], 'countries_distinct_count': 1, 'institutions_distinct_count': 2, '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': 63}, 'biblio': {'volume': None, 'issue': None, 'first_page': '78', 'last_page': '83'}, 'is_retracted': False, 'is_paratext': False, 'primary_topic': {'id': 'https://openalex.org/T10142', 'display_name': 'Formal Methods in Verification', 'score': 1.0, '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': 1.0, '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/T11450', 'display_name': 'Model-Driven Software Engineering Techniques', 'score': 0.9978, '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/T10904', 'display_name': 'Embedded Systems Design Techniques', 'score': 0.997, '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'}}], 'keywords': [{'id': 'https://openalex.org/keywords/runtime-verification', 'display_name': 'Runtime Verification', 'score': 0.6196363}, {'id': 'https://openalex.org/keywords/intelligent-verification', 'display_name': 'Intelligent verification', 'score': 0.5972503}, {'id': 'https://openalex.org/keywords/functional-verification', 'display_name': 'Functional verification', 'score': 0.5737906}, {'id': 'https://openalex.org/keywords/verification', 'display_name': 'Verification', 'score': 0.5296219}, {'id': 'https://openalex.org/keywords/high-level-verification', 'display_name': 'High-level verification', 'score': 0.50699306}, {'id': 'https://openalex.org/keywords/formal-equivalence-checking', 'display_name': 'Formal equivalence checking', 'score': 0.4887769}], 'concepts': [{'id': 'https://openalex.org/C111498074', 'wikidata': 'https://www.wikidata.org/wiki/Q173326', 'display_name': 'Formal verification', 'level': 2, 'score': 0.81900257}, {'id': 'https://openalex.org/C41008148', 'wikidata': 'https://www.wikidata.org/wiki/Q21198', 'display_name': 'Computer science', 'level': 0, 'score': 0.77921605}, {'id': 'https://openalex.org/C75606506', 'wikidata': 'https://www.wikidata.org/wiki/Q1049183', 'display_name': 'Formal methods', 'level': 2, 'score': 0.7273773}, {'id': 'https://openalex.org/C202973057', 'wikidata': 'https://www.wikidata.org/wiki/Q7380130', 'display_name': 'Runtime verification', 'level': 3, 'score': 0.6196363}, {'id': 'https://openalex.org/C3406870', 'wikidata': 'https://www.wikidata.org/wiki/Q6044160', 'display_name': 'Intelligent verification', 'level': 5, 'score': 0.5972503}, {'id': 'https://openalex.org/C62460635', 'wikidata': 'https://www.wikidata.org/wiki/Q5508853', 'display_name': 'Functional verification', 'level': 3, 'score': 0.5737906}, {'id': 'https://openalex.org/C142284323', 'wikidata': 'https://www.wikidata.org/wiki/Q7921323', 'display_name': 'Verification', 'level': 5, 'score': 0.5296219}, {'id': 'https://openalex.org/C187250869', 'wikidata': 'https://www.wikidata.org/wiki/Q5754573', 'display_name': 'High-level verification', 'level': 5, 'score': 0.50699306}, {'id': 'https://openalex.org/C2778869765', 'wikidata': 'https://www.wikidata.org/wiki/Q6028363', 'display_name': 'Inefficiency', 'level': 2, 'score': 0.4922513}, {'id': 'https://openalex.org/C96654402', 'wikidata': 'https://www.wikidata.org/wiki/Q5469962', 'display_name': 'Formal equivalence checking', 'level': 3, 'score': 0.4887769}, {'id': 'https://openalex.org/C116253237', 'wikidata': 'https://www.wikidata.org/wiki/Q1437424', 'display_name': 'Formal specification', 'level': 2, 'score': 0.4627092}, {'id': 'https://openalex.org/C199360897', 'wikidata': 'https://www.wikidata.org/wiki/Q9143', 'display_name': 'Programming language', 'level': 1, 'score': 0.31259498}, {'id': 'https://openalex.org/C149091818', 'wikidata': 'https://www.wikidata.org/wiki/Q2429814', 'display_name': 'Software system', 'level': 3, 'score': 0.09741491}, {'id': 'https://openalex.org/C2777904410', 'wikidata': 'https://www.wikidata.org/wiki/Q7397', 'display_name': 'Software', 'level': 2, 'score': 0.08316222}, {'id': 'https://openalex.org/C186846655', 'wikidata': 'https://www.wikidata.org/wiki/Q3398377', 'display_name': 'Software construction', 'level': 4, 'score': 0.0}, {'id': 'https://openalex.org/C175444787', 'wikidata': 'https://www.wikidata.org/wiki/Q39072', 'display_name': 'Microeconomics', 'level': 1, 'score': 0.0}, {'id': 'https://openalex.org/C162324750', 'wikidata': 'https://www.wikidata.org/wiki/Q8134', 'display_name': 'Economics', 'level': 0, 'score': 0.0}], 'mesh': [], 'locations_count': 1, 'locations': [{'is_oa': False, 'landing_page_url': 'https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.413.323&rep=rep1&type=pdf', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S4306419863', 'display_name': 'International Conference on Systems', 'issn_l': None, 'issn': None, 'is_oa': False, 'is_in_doaj': False, 'is_core': False, 'host_organization': None, 'host_organization_name': None, 'host_organization_lineage': [], 'host_organization_lineage_names': [], 'type': 'conference'}, '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': 9, 'referenced_works': ['https://openalex.org/W1503170978', 'https://openalex.org/W1540522725', 'https://openalex.org/W1559035930', 'https://openalex.org/W1582385421', 'https://openalex.org/W174127401', 'https://openalex.org/W1943502734', 'https://openalex.org/W2102461075', 'https://openalex.org/W2160823654', 'https://openalex.org/W68069235'], 'related_works': ['https://openalex.org/W2828412611', 'https://openalex.org/W2596418697', 'https://openalex.org/W2367198932', 'https://openalex.org/W2168362805', 'https://openalex.org/W2167022220', 'https://openalex.org/W2162615969', 'https://openalex.org/W2141443374', 'https://openalex.org/W2136208798', 'https://openalex.org/W2134877784', 'https://openalex.org/W2124025245', 'https://openalex.org/W2109821323', 'https://openalex.org/W2094686007', 'https://openalex.org/W2060099438', 'https://openalex.org/W1973369219', 'https://openalex.org/W1623421902', 'https://openalex.org/W1602916281', 'https://openalex.org/W1495911618', 'https://openalex.org/W1484544740', 'https://openalex.org/W146350398', 'https://openalex.org/W1140958732'], 'abstract_inverted_index': {'In': [0], 'design': [1], 'of': [2, 31], 'complex': [3], 'and': [4], 'large': [5], 'scale': [6], 'systems,': [7], 'formal': [8, 38, 56], 'verification': [9], 'has': [10], 'played': [11], 'an': [12], 'important': [13], 'role.': [14], 'However,': [15], 'it': [16], 'is': [17], 'inefficiency': [18], 'to': [19], 'verify': [20], 'the': [21, 27], 'entire': [22], 'systems.': [23], 'This': [24], 'article': [25], 'considers': [26], 'case': [28], 'where': [29], 'designers': [30], 'systems': [32], 'can': [33, 49], 'extract': [34], 'check-points': [35], 'easily': [36], 'in': [37, 55], 'verification.': [39, 57], 'Moreover,': [40], 'we': [41], 'propose': [42], 'a': [43], 'method': [44], 'by': [45], 'which': [46], 'temporal': [47], 'formulas': [48], 'be': [50], 'obtained': [51], 'inductively': [52], 'for': [53], 'specifications': [54]}, 'cited_by_api_url': 'https://api.openalex.org/works?filter=cites:W161255303', 'counts_by_year': [], 'updated_date': '2024-12-13T08:59:26.819962', 'created_date': '2016-06-24'}
Publication Information

Basic Information

Access and Citation

AI Researcher Chatbot

Primary Location

Authors

Topics

Keywords

Related Works
