Mercurial > hg > Papers > 2020 > anatofuz-sigos
changeset 49:72805ecaa331
...
| author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 07 May 2020 19:10:57 +0900 |
| parents | 567288b8a89e |
| children | 5f09000649ef |
| files | paper/anatofuz-bib.bib paper/anatofuz-sigos.md paper/anatofuz-sigos.pdf paper/anatofuz-sigos.tex |
| diffstat | 4 files changed, 2 insertions(+), 29 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/anatofuz-bib.bib Thu May 07 19:04:11 2020 +0900 +++ b/paper/anatofuz-bib.bib Thu May 07 19:10:57 2020 +0900 @@ -19,27 +19,6 @@ year = 2015 } -@article{moggi-monad, - author = {Moggi, Eugenio}, - title = {Notions of Computation and Monads}, - journal = {Inf. Comput.}, - issue_date = {July 1991}, - volume = {93}, - number = {1}, - month = jul, - year = {1991}, - issn = {0890-5401}, - pages = {55--92}, - numpages = {38}, - url = {http://dx.doi.org/10.1016/0890-5401(91)90052-4}, - doi = {10.1016/0890-5401(91)90052-4}, - acmid = {116984}, - publisher = {Academic Press, Inc.}, - address = {Duluth, MN, USA}, - -} - - @inproceedings{Yang:2010:SLI:1806596.1806610, author = {Yang, Jean and Hawblitzel, Chris}, @@ -178,11 +157,6 @@ year = 2016 } -@manual{arm, -author = "{ARM Architecture Reference Manual}", -title = "{http://infocenter.arm.com/help/topic/com.arm.\\doc.subset.architecture.reference/index.html}" -} - @misc{xv6, author = "{Russ Cox, Frans Kaashoek, Robert Morris}", title = {xv6 a simple, Unix-like teaching operating system}, @@ -190,7 +164,6 @@ } - @inproceedings{Chen:2015:UCH:2815400.2815402, author = {Chen, Haogang and Ziegler, Daniel and Chajed, Tej and Chlipala, Adam and Kaashoek, M. Frans and Zeldovich, Nickolai}, title = {Using Crash Hoare Logic for Certifying the FSCQ File System},
--- a/paper/anatofuz-sigos.md Thu May 07 19:04:11 2020 +0900 +++ b/paper/anatofuz-sigos.md Thu May 07 19:10:57 2020 +0900 @@ -5,7 +5,7 @@ テスト以外の方法でOSの信頼性を高めたい。 そこで数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。 -OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、定理証明支援系Agda\cite{agda}を利用した証明ベースでの信頼性の確保などの手法が考えられる。\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} +OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、定理証明支援系Agda\cite{agda}を利用した証明ベースでの信頼性の確保などの手法が考えられる。\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402} 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。\cite{hyperKernel} OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。 しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。
--- a/paper/anatofuz-sigos.tex Thu May 07 19:04:11 2020 +0900 +++ b/paper/anatofuz-sigos.tex Thu May 07 19:10:57 2020 +0900 @@ -83,7 +83,7 @@ テスト以外の方法でOSの信頼性を高めたい。 そこで数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。 -OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、定理証明支援系Agda\cite{agda}を利用した証明ベースでの信頼性の確保などの手法が考えられる。\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} +OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、定理証明支援系Agda\cite{agda}を利用した証明ベースでの信頼性の確保などの手法が考えられる。\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402} 形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。\cite{hyperKernel} OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。 しかし仕様記述言語や定理証明支援系では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などでの実装の段階で発生するバグを取り除くことができない。