WEKO3
インデックスリンク
アイテム
{"_buckets": {"deposit": "3c763b33-c71e-4b1f-bdbc-a79bf4e858ee"}, "_deposit": {"created_by": 3, "id": "8988", "owners": [3], "pid": {"revision_id": 0, "type": "depid", "value": "8988"}, "status": "published"}, "_oai": {"id": "oai:kanazawa-u.repo.nii.ac.jp:00008988", "sets": ["936"]}, "author_link": ["397", "12772", "12773", "12774"], "item_4_biblio_info_8": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2013-05-24", "bibliographicIssueDateType": "Issued"}, "bibliographicIssueNumber": "6649888", "bibliographicPageEnd": "608", "bibliographicPageStart": "607", "bibliographic_titles": [{"bibliographic_title": "Proceedings - International Computer Software and Applications Conference"}]}]}, "item_4_description_21": {"attribute_name": "抄録", "attribute_value_mlt": [{"subitem_description": "Dynamically reconfigurable systems have attracted public attention from the point of view of miniaturization and saving power consumption for embedded systems in recent years. In this study, we propose dynamic linear hybrid automata as specification language of dynamically reconfigurable systems and the verification technique of reachability analysis. A dynamic linear hybrid automaton(DLHA) is a linear hybrid automaton extended with actions of creation and destruction. This paper presents the model checker and applies it to the model of an embedded system consisting CPU and DRP. © 2013 IEEE.", "subitem_description_type": "Abstract"}]}, "item_4_publisher_17": {"attribute_name": "出版者", "attribute_value_mlt": [{"subitem_publisher": "IEEE"}]}, "item_4_relation_12": {"attribute_name": "DOI", "attribute_value_mlt": [{"subitem_relation_type": "isVersionOf", "subitem_relation_type_id": {"subitem_relation_type_id_text": "10.1109/COMPSAC.2013.98", "subitem_relation_type_select": "DOI"}}]}, "item_4_source_id_9": {"attribute_name": "ISSN", "attribute_value_mlt": [{"subitem_source_identifier": "0730-3157", "subitem_source_identifier_type": "ISSN"}]}, "item_4_version_type_25": {"attribute_name": "著者版フラグ", "attribute_value_mlt": [{"subitem_version_resource": "http://purl.org/coar/version/c_ab4af688f83e57aa", "subitem_version_type": "AM"}]}, "item_creator": {"attribute_name": "著者", "attribute_type": "creator", "attribute_value_mlt": [{"creatorNames": [{"creatorName": "Yanase, Ryo"}], "nameIdentifiers": [{"nameIdentifier": "12772", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Sakai, Tatsunori"}], "nameIdentifiers": [{"nameIdentifier": "12773", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Sakai, Makoto"}], "nameIdentifiers": [{"nameIdentifier": "12774", "nameIdentifierScheme": "WEKO"}]}, {"creatorNames": [{"creatorName": "Yamane, Satoshi"}], "nameIdentifiers": [{"nameIdentifier": "397", "nameIdentifierScheme": "WEKO"}, {"nameIdentifier": "70263506", "nameIdentifierScheme": "金沢大学研究者情報", "nameIdentifierURI": "http://ridb.kanazawa-u.ac.jp/public/detail.php?kaken=70263506"}, {"nameIdentifier": "70263506", "nameIdentifierScheme": "研究者番号", "nameIdentifierURI": "https://nrid.nii.ac.jp/nrid/1000070263506"}]}]}, "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-YANASE-R-607.pdf", "filesize": [{"value": "140.9 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_free", "mimetype": "application/pdf", "size": 140900.0, "url": {"label": "TE-PR-YANASE-R-607.pdf", "url": "https://kanazawa-u.repo.nii.ac.jp/record/8988/files/TE-PR-YANASE-R-607.pdf"}, "version_id": "9c1416d2-0051-4286-9bea-67271858afdf"}]}, "item_keyword": {"attribute_name": "キーワード", "attribute_value_mlt": [{"subitem_subject": "Dynamically reconfigurable systems", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Hybrid automata", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Model checking", "subitem_subject_scheme": "Other"}, {"subitem_subject": "Verification", "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": "Development of model checker of dynamic linear hybrid automata", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "Development of model checker of dynamic linear hybrid automata"}]}, "item_type_id": "4", "owner": "3", "path": ["936"], "permalink_uri": "http://hdl.handle.net/2297/36977", "pubdate": {"attribute_name": "公開日", "attribute_value": "2017-10-03"}, "publish_date": "2017-10-03", "publish_status": "0", "recid": "8988", "relation": {}, "relation_version_is_last": true, "title": ["Development of model checker of dynamic linear hybrid automata"], "weko_shared_id": -1}
Development of model checker of dynamic linear hybrid automata
http://hdl.handle.net/2297/36977
http://hdl.handle.net/2297/369771a7b4df5-c802-45e8-bf6f-1499b12c67d0
名前 / ファイル | ライセンス | アクション |
---|---|---|
TE-PR-YANASE-R-607.pdf (140.9 kB)
|
|
Item type | 学術雑誌論文 / Journal Article(1) | |||||
---|---|---|---|---|---|---|
公開日 | 2017-10-03 | |||||
タイトル | ||||||
タイトル | Development of model checker of dynamic linear hybrid automata | |||||
言語 | ||||||
言語 | eng | |||||
資源タイプ | ||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
資源タイプ | journal article | |||||
著者 |
Yanase, Ryo
× Yanase, Ryo× Sakai, Tatsunori× Sakai, Makoto× Yamane, Satoshi |
|||||
書誌情報 |
Proceedings - International Computer Software and Applications Conference 号 6649888, p. 607-608, 発行日 2013-05-24 |
|||||
ISSN | ||||||
収録物識別子タイプ | ISSN | |||||
収録物識別子 | 0730-3157 | |||||
DOI | ||||||
関連タイプ | isVersionOf | |||||
識別子タイプ | DOI | |||||
関連識別子 | 10.1109/COMPSAC.2013.98 | |||||
出版者 | ||||||
出版者 | IEEE | |||||
抄録 | ||||||
内容記述タイプ | Abstract | |||||
内容記述 | Dynamically reconfigurable systems have attracted public attention from the point of view of miniaturization and saving power consumption for embedded systems in recent years. In this study, we propose dynamic linear hybrid automata as specification language of dynamically reconfigurable systems and the verification technique of reachability analysis. A dynamic linear hybrid automaton(DLHA) is a linear hybrid automaton extended with actions of creation and destruction. This paper presents the model checker and applies it to the model of an embedded system consisting CPU and DRP. © 2013 IEEE. | |||||
著者版フラグ | ||||||
出版タイプ | AM | |||||
出版タイプResource | http://purl.org/coar/version/c_ab4af688f83e57aa |