Mercurial > hg > Papers > 2021 > anatofuz-master

comparison paper/chapter/introduction.tex @ 15:36d241194507

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Thu, 28 Jan 2021 20:47:08 +0900
parents e543ba9a8e5c
children c69811b44e7c
comparison
equal deleted inserted replaced
14:7c6d3d582554 15:36d241194507
15 またOSはCPU制御やメモリ制御、 並列・並行処理などを多用する。 15 またOSはCPU制御やメモリ制御、 並列・並行処理などを多用する。
16 テストコードを用いて処理を検証する場合、テストコードとして特定の状況を作成する必要がある。 16 テストコードを用いて処理を検証する場合、テストコードとして特定の状況を作成する必要がある。
17 実際にOSが動作する中でバグやエラーを発生する条件を、 並列処理の状況などを踏まえてテストコードで表現するのは困難である。 17 実際にOSが動作する中でバグやエラーを発生する条件を、 並列処理の状況などを踏まえてテストコードで表現するのは困難である。
18 非決定的な処理を持つOSの信頼性を保証するには、 テストコード以外の手法を用いる必要がある。 18 非決定的な処理を持つOSの信頼性を保証するには、 テストコード以外の手法を用いる必要がある。
19 19
20
20 テストコード以外の方法として、 形式手法的と呼ばれるアプローチがある。 21 テストコード以外の方法として、 形式手法的と呼ばれるアプローチがある。
21 形式手法の具体的な検証方法の中で、 証明を用いる方法とモデル検査を用いる方法がある。 22 形式手法の具体的な検証方法の中で、 証明を用いる方法とモデル検査を用いる方法がある。
22 証明を用いる方法ではAgdaやCoqなどの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。 23 証明を用いる方法ではAgdaやCoqなどの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。
23 Curry-Howard同型対応則により、型と命題が、 プログラムと証明が対応する。 24 Curry-Howard同型対応則により、型と論理式の命題が対応する。
25 この型を導出するプログラムと実際の証明が対応する。
26 特定の型を入力として受け取り、証明したい型を生成する関数を作成する。
27 証明そのものは記述した関数の内容の整合性を、定理証明支援系が検証する。
28 証明を使う手法の場合、 実際の証明を行うのは定理証明支援系であるため、 定理証明支援系が理解できるプログラムで実装する必要がある。
29 AgdaやCoqの場合はAgda、 Cow自身のプログラムで記述する必要がある。
30 しかしAgdaで証明ができてもAgdaのコードを直接OSのソースコードとしてコンパイルすることはできない。
31 Agda側でCのソースコードを吐き出せれば可能ではあるが、 現状は検証したコードと実際に動作するコードは分離されている。
32 検証ができているソースコードそのものを使ってOSを動作させたい。
33
34
35 他の形式手法にモデル検査がある。
36 モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。
37 モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。
38 実装するコードに対してモデル検査を行いたいが、モデル検査を行うモデル検査器は限られている。
39 例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。