WEKO3
インデックスリンク
アイテム
{"_buckets": {"deposit": "90bda043-84fe-4fcb-a7cb-47047d2d202c"}, "_deposit": {"created_by": 3, "id": "7465", "owners": [3], "pid": {"revision_id": 0, "type": "depid", "value": "7465"}, "status": "published"}, "_oai": {"id": "oai:kanazawa-u.repo.nii.ac.jp:00007465", "sets": ["936"]}, "author_link": ["397"], "item_8_biblio_info_8": {"attribute_name": "書誌情報", "attribute_value_mlt": [{"bibliographicIssueDates": {"bibliographicIssueDate": "2003-01-01", "bibliographicIssueDateType": "Issued"}, "bibliographicPageEnd": "533", "bibliographicPageStart": "527", "bibliographic_titles": [{"bibliographic_title": "Proceedings - IEEE Computer Society\u0027s International Computer Software and Applications Conference"}]}]}, "item_8_description_21": {"attribute_name": "抄録", "attribute_value_mlt": [{"subitem_description": "Real-time software runs over real-time operating systems, and guaranteeing Qualities is difficult. As timing constraints and resource allocations are strict, it is necessary to verify schedulability, safety and liveness properties. In this paper, we formally specify real-time software using hybrid automata and verify its schedulability using both deductive refinement theory and scheduling theory. In this case, the above real-time software consists of periodic processes and a fixed-priority preemptive scheduling policy on one CPU. Using our proposed methods, we can uniformally and easily specify real-time software and verify its schedulability based on hybrid automata. Moreover, we can verify its schedulability at design stage.", "subitem_description_type": "Abstract"}]}, "item_8_publisher_17": {"attribute_name": "出版者", "attribute_value_mlt": [{"subitem_publisher": "Institute of Electrical and Electronics Engineers (IEEE)"}]}, "item_8_source_id_9": {"attribute_name": "ISSN", "attribute_value_mlt": [{"subitem_source_identifier": "0730-6512", "subitem_source_identifier_type": "ISSN"}]}, "item_8_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": "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-YAMANE-S-527.pdf", "filesize": [{"value": "735.5 kB"}], "format": "application/pdf", "future_date_message": "", "is_thumbnail": false, "licensetype": "license_free", "mimetype": "application/pdf", "size": 735500.0, "url": {"label": "TE-PR-YAMANE-S-527.pdf", "url": "https://kanazawa-u.repo.nii.ac.jp/record/7465/files/TE-PR-YAMANE-S-527.pdf"}, "version_id": "cb05c332-31bb-4423-8074-56005efb858a"}]}, "item_language": {"attribute_name": "言語", "attribute_value_mlt": [{"subitem_language": "eng"}]}, "item_resource_type": {"attribute_name": "資源タイプ", "attribute_value_mlt": [{"resourcetype": "conference paper", "resourceuri": "http://purl.org/coar/resource_type/c_5794"}]}, "item_title": "Deductive Schedulability Verification Methodology of Real-Time Software using both Refinement Verification and Hybrid Automata", "item_titles": {"attribute_name": "タイトル", "attribute_value_mlt": [{"subitem_title": "Deductive Schedulability Verification Methodology of Real-Time Software using both Refinement Verification and Hybrid Automata"}]}, "item_type_id": "8", "owner": "3", "path": ["936"], "permalink_uri": "http://hdl.handle.net/2297/6708", "pubdate": {"attribute_name": "公開日", "attribute_value": "2017-10-03"}, "publish_date": "2017-10-03", "publish_status": "0", "recid": "7465", "relation": {}, "relation_version_is_last": true, "title": ["Deductive Schedulability Verification Methodology of Real-Time Software using both Refinement Verification and Hybrid Automata"], "weko_shared_id": -1}
Deductive Schedulability Verification Methodology of Real-Time Software using both Refinement Verification and Hybrid Automata
http://hdl.handle.net/2297/6708
http://hdl.handle.net/2297/670888319aa0-ee13-4a1f-92d2-14dfa80640c4
名前 / ファイル | ライセンス | アクション |
---|---|---|
TE-PR-YAMANE-S-527.pdf (735.5 kB)
|
|
Item type | 会議発表論文 / Conference Paper(1) | |||||
---|---|---|---|---|---|---|
公開日 | 2017-10-03 | |||||
タイトル | ||||||
タイトル | Deductive Schedulability Verification Methodology of Real-Time Software using both Refinement Verification and Hybrid Automata | |||||
言語 | ||||||
言語 | eng | |||||
資源タイプ | ||||||
資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||
資源タイプ | conference paper | |||||
著者 |
Yamane, Satoshi
× Yamane, Satoshi |
|||||
書誌情報 |
Proceedings - IEEE Computer Society's International Computer Software and Applications Conference p. 527-533, 発行日 2003-01-01 |
|||||
ISSN | ||||||
収録物識別子タイプ | ISSN | |||||
収録物識別子 | 0730-6512 | |||||
出版者 | ||||||
出版者 | Institute of Electrical and Electronics Engineers (IEEE) | |||||
抄録 | ||||||
内容記述タイプ | Abstract | |||||
内容記述 | Real-time software runs over real-time operating systems, and guaranteeing Qualities is difficult. As timing constraints and resource allocations are strict, it is necessary to verify schedulability, safety and liveness properties. In this paper, we formally specify real-time software using hybrid automata and verify its schedulability using both deductive refinement theory and scheduling theory. In this case, the above real-time software consists of periodic processes and a fixed-priority preemptive scheduling policy on one CPU. Using our proposed methods, we can uniformally and easily specify real-time software and verify its schedulability based on hybrid automata. Moreover, we can verify its schedulability at design stage. | |||||
著者版フラグ | ||||||
出版タイプ | VoR | |||||
出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 |