WEKO3
アイテム
GearsOSとgearsAgda上のモデル検査について
https://ipsj.ixsq.nii.ac.jp/records/241050
https://ipsj.ixsq.nii.ac.jp/records/24105009668492-ed5e-43d6-9231-8b6ca670ae06
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-ComSys2024003.pdf (1.6 MB)
2026年11月25日からダウンロード可能です。
|
Copyright (c) 2024 by the Information Processing Society of Japan
|
|
| 非会員：¥660, IPSJ:学会員：¥330, OS:会員：¥0, DLIB:会員：¥0 | ||
| Item type | Symposium(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2024-11-25 | |||||||
| タイトル | ||||||||
| タイトル | GearsOSとgearsAgda上のモデル検査について | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Model checking on GearsOS and gearsAgda | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||
| 資源タイプ | conference paper | |||||||
| 著者所属 | ||||||||
| 現在，琉球大学 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Presently with Uniersity of the Ryukyus | ||||||||
| 著者名 |
河野, 真治
× 河野, 真治
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | GearsOS は軽量継続を用いて，さまざまなプログラムを記述する．この時の記述言語として C base の CbC (Continuation based C) と，Agda baseのgearsAgda がある．CbC で記述されたプログラムは Model 検査することができるが，それには計算量がかかる．geasAgda で記述されたプログラムは，Invariant をメタレベルに導入することでさまざまな検証をおこなうことができる この論文では gearsAgda を使ったモデル検査について述べる．Buchi automaton と時相論理式の記述を Agda で記述し，それを Invariant として gearsAgda の code にいれることで検証をおこなう．gearsAgdaのfair scheduler で実行せずに，検証を行うことが可能になる したがって，正確にはモデル検査的な手法を用いたプログラムの検証になる | |||||||
| 書誌情報 |
コンピュータシステム・シンポジウム論文集 巻 2024, p. 17-20, 発行日 2024-11-25 |
|||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
