view paper/introduction.tex @ 5:196ba119ca89

fix, and add mindmap->pdf
author ryokka
date Mon, 03 Feb 2020 21:47:43 +0900
parents 41a936510fd0
children d30593612a38
line wrap: on
line source

% sigos のやつ
\chapter{プログラミング言語の検証}
\label{chapter:intro}
現在の OS やアプリケーションの検証では、実装と別に検証用の言語で記述された実装と証明を持つのが一般的である。
kernel 検証\cite{Klein:2010:SFV:1743546.1743574},\cite{Nelson:2017:HPV:3132747.3132748}の例では C で記述された Kernel に対して、検証用の別の言語で書かれた等価な kernel を用いて OS の検証を行っている。
また、別のアプローチとしては ATS2\cite{ats2} や Rust\cite{rust} などの低レベル記述向けの関数型言語を実装に用いる手法が存在している。

証明支援向けのプログラミング言語としては Agda\cite{agda}、 Coq\cite{coq} などが存在しているが、これらの言語自体は実行速度が期待できるものではない。

そこで、当研究室では検証と実装が同一の言語で行う Continuation based C\cite{cbc} という言語を開発している。
Continuation based C(CbC) では、処理の単位を CodeGear、 データの単位を DataGear としている。
CodeGear は値を入力として受け取り出力を行う処理の単位であり、 CodeGear の出力を 次の GodeGear に接続してプログラミングを行う。 CodeGear の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行うことができる。
このメタ計算部分で assertion などの検証を行うことで、 CodeGear の処理に手を加えることなく検証を行う。
現段階では CbC 自体に証明を行うためのシステムが存在しないため、証明支援系言語である Agda を用いて等価な実装の検証を行っている。


%現代の OS では拡張性と信頼性を両立させることが要求されている。
%時代と主に進歩するハードウェア、サービスに対して OS 自体が拡張される必要がある。
%しかし、OSには非決定的な実行を持っており、その信頼性を保証するには従来のテストとデバッグでは不十分であり、テスト仕切れない部分が残ってしまう。
%これに対処するために証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。
% 証明やモデル検査を用いて OS の検証する方法は様々なものが検討されている。
% 型付きアセンブラ\cite{Yang:2010:SLI:1806596.1806610}
% 従来の研究ではPython\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596}による記述した OS を検証する研究も存在する。
% また SPIN などのモデル検査を OS の検証に用いた例もである。
% 本研究室では信頼性をノーマルレベルの掲載に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を開発している。