WEKO3
インデックスリンク
アイテム
{"_buckets": {"deposit": "9659ec9a-2866-46cd-9ab5-45287c5fc0a0"}, "_deposit": {"created_by": 3, "id": "9771", "owners": [3], "pid": {"revision_id": 0, "type": "depid", "value": "9771"}, "status": "published"}, "_oai": {"id": "oai:kanazawa-u.repo.nii.ac.jp:00009771", "sets": ["936"]}, "author_link": ["14274", "402"], "item_4_biblio_info_8": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2009-01-01", "bibliographicIssueDateType": "Issued"}, "bibliographicIssueNumber": "5", "bibliographicPageEnd": "1021", "bibliographicPageStart": "1012", "bibliographicVolumeNumber": "E92-D", "bibliographic_titles": [{"bibliographic_title": "IEICE Transactions on Information and Systems"}]}]}, "item_4_description_21": {"attribute_name": "抄録", "attribute_value_mlt": [{"subitem_description": "In the OTS/CafeOBJ method, software specifications are described in CafeOBJ executable formal specification language, and verification is done by giving scripts to the CafeOBJ system. The script is called a proof score. In this study, we propose a test case generator from an OTS/CafeOBJ specification together with a proof score. Our test case generator gives test cases by analyzing the proof score. The test cases are used to test whether an implementation satisfies the specification and the property verified by the proof score. Since a proof score involves important information for verifying a property, the generated test cases are also expected to be suitable to test the property. Copyright © 2009 The Institute of Electronics, Information and Communication Engineers.", "subitem_description_type": "Abstract"}]}, "item_4_description_5": {"attribute_name": "提供者所属", "attribute_value_mlt": [{"subitem_description": "金沢大学理工研究域電子情報学系", "subitem_description_type": "Other"}]}, "item_4_publisher_17": {"attribute_name": "出版者", "attribute_value_mlt": [{"subitem_publisher": "The Institute of Electronics, Information and Communication Engineers = 電子情報通信学会"}]}, "item_4_relation_12": {"attribute_name": "DOI", "attribute_value_mlt": [{"subitem_relation_type": "isIdenticalTo", "subitem_relation_type_id": {"subitem_relation_type_id_text": "10.1587/transinf.E92.D.1012", "subitem_relation_type_select": "DOI"}}]}, "item_4_source_id_11": {"attribute_name": "NCID", "attribute_value_mlt": [{"subitem_source_identifier": "AA10826272", "subitem_source_identifier_type": "NCID"}]}, "item_4_source_id_9": {"attribute_name": "ISSN", "attribute_value_mlt": [{"subitem_source_identifier": "0916-8532", "subitem_source_identifier_type": "ISSN"}]}, "item_4_version_type_25": {"attribute_name": "著者版フラグ", "attribute_value_mlt": [{"subitem_version_resource": "http://purl.org/coar/version/c_970fb48d4fbd8a85", "subitem_version_type": "VoR"}]}, "item_creator": {"attribute_name": "著者", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "Nakamura, Masaki"}], "nameIdentifiers": [{"nameIdentifier": "402", "nameIdentifierScheme": "WEKO"}, {"nameIdentifier": "40345658", "nameIdentifierScheme": "研究者番号", "nameIdentifierURI": "https://nrid.nii.ac.jp/nrid/1000040345658"}]}, {"creatorNames": [{"creatorName": "Seino, Takahiro"}], "nameIdentifiers": [{"nameIdentifier": "14274", "nameIdentifierScheme": "WEKO"}]}]}, "item_files": {"attribute_name": "ファイル情報", "attribute_type": "file", "attribute_value_mlt": [{"accessrole": "open_date", "date": [{"dateType": "Available", "dateValue": "2017-10-03"}], "displaytype": "detail", "download_preview_message": "", "file_order": 0, "filename": "TE-PR-NAKAMURA-M-1012.pdf", "filesize": [{"value": "237.4 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_free", "mimetype": "application/pdf", "size": 237400.0, "url": {"label": "TE-PR-NAKAMURA-M-1012.pdf", "url": "https://kanazawa-u.repo.nii.ac.jp/record/9771/files/TE-PR-NAKAMURA-M-1012.pdf"}, "version_id": "1cd0bee2-432a-4e4a-9a51-b875086d22f1"}]}, "item_keyword": {"attribute_name": "キーワード", "attribute_value_mlt": [{"subitem_subject": "CafeOBJ", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Formal specification", "subitem_subject_scheme": "Other"}, {"subitem_subject": "OTS", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Proof score", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Software testing", "subitem_subject_scheme": "Other"}]}, "item_language": {"attribute_name": "言語", "attribute_value_mlt": [{"subitem_language": "eng"}]}, "item_resource_type": {"attribute_name": "資源タイプ", "attribute_value_mlt": [{"resourcetype": "journal article", "resourceuri": "http://purl.org/coar/resource_type/c_6501"}]}, "item_title": "Generating test cases for invariant properties from proof scores in the OTS/CafeOBJ method", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "Generating test cases for invariant properties from proof scores in the OTS/CafeOBJ method"}]}, "item_type_id": "4", "owner": "3", "path": ["936"], "permalink_uri": "http://hdl.handle.net/2297/23903", "pubdate": {"attribute_name": "公開日", "attribute_value": "2017-10-03"}, "publish_date": "2017-10-03", "publish_status": "0", "recid": "9771", "relation": {}, "relation_version_is_last": true, "title": ["Generating test cases for invariant properties from proof scores in the OTS/CafeOBJ method"], "weko_shared_id": -1}
Generating test cases for invariant properties from proof scores in the OTS/CafeOBJ method
http://hdl.handle.net/2297/23903
http://hdl.handle.net/2297/23903a101530e-0fe1-48e6-9d73-0092cc64e867
名前 / ファイル | ライセンス | アクション |
---|---|---|
TE-PR-NAKAMURA-M-1012.pdf (237.4 kB)
|
|
Item type | 学術雑誌論文 / Journal Article(1) | |||||
---|---|---|---|---|---|---|
公開日 | 2017-10-03 | |||||
タイトル | ||||||
タイトル | Generating test cases for invariant properties from proof scores in the OTS/CafeOBJ method | |||||
言語 | ||||||
言語 | eng | |||||
資源タイプ | ||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
資源タイプ | journal article | |||||
著者 |
Nakamura, Masaki
× Nakamura, Masaki× Seino, Takahiro |
|||||
提供者所属 | ||||||
内容記述タイプ | Other | |||||
内容記述 | 金沢大学理工研究域電子情報学系 | |||||
書誌情報 |
IEICE Transactions on Information and Systems 巻 E92-D, 号 5, p. 1012-1021, 発行日 2009-01-01 |
|||||
ISSN | ||||||
収録物識別子タイプ | ISSN | |||||
収録物識別子 | 0916-8532 | |||||
NCID | ||||||
収録物識別子タイプ | NCID | |||||
収録物識別子 | AA10826272 | |||||
DOI | ||||||
関連タイプ | isIdenticalTo | |||||
識別子タイプ | DOI | |||||
関連識別子 | 10.1587/transinf.E92.D.1012 | |||||
出版者 | ||||||
出版者 | The Institute of Electronics, Information and Communication Engineers = 電子情報通信学会 | |||||
抄録 | ||||||
内容記述タイプ | Abstract | |||||
内容記述 | In the OTS/CafeOBJ method, software specifications are described in CafeOBJ executable formal specification language, and verification is done by giving scripts to the CafeOBJ system. The script is called a proof score. In this study, we propose a test case generator from an OTS/CafeOBJ specification together with a proof score. Our test case generator gives test cases by analyzing the proof score. The test cases are used to test whether an implementation satisfies the specification and the property verified by the proof score. Since a proof score involves important information for verifying a property, the generated test cases are also expected to be suitable to test the property. Copyright © 2009 The Institute of Electronics, Information and Communication Engineers. | |||||
著者版フラグ | ||||||
出版タイプ | VoR | |||||
出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 |