{"created":"2023-07-27T06:25:37.137719+00:00","id":8988,"links":{},"metadata":{"_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":["934:935: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":[{}]},{"creatorNames":[{"creatorName":"Sakai, Tatsunori"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Sakai, Makoto"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Yamane, Satoshi"}],"nameIdentifiers":[{},{},{}]}]},"item_files":{"attribute_name":"ファイル情報","attribute_type":"file","attribute_value_mlt":[{"accessrole":"open_date","date":[{"dateType":"Available","dateValue":"2017-10-03"}],"displaytype":"detail","filename":"TE-PR-YANASE-R-607.pdf","filesize":[{"value":"140.9 kB"}],"format":"application/pdf","licensetype":"license_note","mimetype":"application/pdf","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_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"],"pubdate":{"attribute_name":"公開日","attribute_value":"2017-10-03"},"publish_date":"2017-10-03","publish_status":"0","recid":"8988","relation_version_is_last":true,"title":["Development of model checker of dynamic linear hybrid automata"],"weko_creator_id":"3","weko_shared_id":-1},"updated":"2023-07-28T02:00:48.060723+00:00"}