{"metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00095552","sets":["1164:1384:7092:7289"]},"path":["7289"],"owner":"11","recid":"95552","title":["組込みCISCマイコンのアセンブリプログラムに対する振舞い抽出器の開発とモデル検査への適用～シミュレーションによるモデルの自動生成～"],"pubdate":{"attribute_name":"公開日","attribute_value":"2013-10-17"},"_buckets":{"deposit":"8dc1ee8c-89e1-4a9b-aeae-6b1b0e76a9da"},"_deposit":{"id":"95552","pid":{"type":"depid","value":"95552","revision_id":0},"owners":[11],"status":"published","created_by":11},"item_title":"組込みCISCマイコンのアセンブリプログラムに対する振舞い抽出器の開発とモデル検査への適用～シミュレーションによるモデルの自動生成～","author_link":["0","0"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"組込みCISCマイコンのアセンブリプログラムに対する振舞い抽出器の開発とモデル検査への適用～シミュレーションによるモデルの自動生成～"},{"subitem_title":"Development of the Behavior Extractor for Assembly Program of Embedded CISC Microcomputer and Adapting to Model Checking - Generating the Model Automatically by Simulation -","subitem_title_language":"en"}]},"item_type_id":"4","publish_date":"2013-10-17","item_4_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"金沢大学"},{"subitem_text_value":"金沢大学"},{"subitem_text_value":"金沢大学"}]},"item_4_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Kanazawa University","subitem_text_language":"en"},{"subitem_text_value":"Kanazawa University","subitem_text_language":"en"},{"subitem_text_value":"Kanazawa University","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"jpn"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":-1,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/95552/files/IPSJ-SE13182002.pdf"},"date":[{"dateType":"Available","dateValue":"2100-01-01"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-SE13182002.pdf","filesize":[{"value":"612.3 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"0","billingrole":"12"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"d11a7cdf-7bf2-4d04-941c-1472bc253b48","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2013 by the Institute of Electronics, Information and Communication Engineers\nThis SIG report is only available to those in membership of the SIG."}]},"item_4_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"公下, 亮佑"},{"creatorName":"山根, 智"},{"creatorName":"櫻井, 孝平"}],"nameIdentifiers":[{}]}]},"item_4_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Ryousuke, Konoshita","creatorNameLang":"en"},{"creatorName":"Satoshi, Yamane","creatorNameLang":"en"},{"creatorName":"Kouhei, Sakurai","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_4_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AN10112981","subitem_source_identifier_type":"NCID"}]},"item_4_textarea_12":{"attribute_name":"Notice","attribute_value_mlt":[{"subitem_textarea_value":"SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc."}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_18gh","resourcetype":"technical report"}]},"item_4_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"我々は，組込みシステムに対してモデル検査することを目的とする．そこで，本論文では，モデルを自動的に構築する，振舞い抽出器の概要について述べる．また，開発する上で困難となる要因と，解決方法について述べる．この抽出器は，状態爆発を起こす可能性があり，特に割り込みやリアクティブ性が，大きな影響を与えている．割り込みは，マスクビットなどから割り込み発生箇所を特定することができる．そのため，考慮する必要のない割り込みを取り除き，状態爆発を抑制できる．リアクティブ性は，不定値で表現することで状態爆発を軽減する．これは，ある値に対して，ピット単位での抽象的な表現を可能にしたものである．","subitem_description_type":"Other"}]},"item_4_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"We aim at Model Checking for Embedded Systems. We describe the outline of Behavior Extractor that automatically constructs a model. Also we describe factors that make it difficult to develop. Extractor have possi bility of the state explosion. In particular, interruption and reactive nature affect it. Interruption can be specified by masking bits. Therefore, it is possible to remove unnecessary interruption and to avoid the state explosion. Reactive nature is represented by Undefined Value, and it can decrease possibility of the state explosion. It is enabled by abstract representation of a bit-by-bit for certain values.","subitem_description_type":"Other"}]},"item_4_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographicPageEnd":"6","bibliographic_titles":[{"bibliographic_title":"研究報告ソフトウェア工学（SE）"}],"bibliographicPageStart":"1","bibliographicIssueDates":{"bibliographicIssueDate":"2013-10-17","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"2","bibliographicVolumeNumber":"2013-SE-182"}]},"relation_version_is_last":true,"weko_creator_id":"11"},"updated":"2025-01-21T13:45:06.846598+00:00","created":"2025-01-18T23:42:36.207365+00:00","links":{},"id":95552}