Mercurial > hg > Papers > 2021 > anatofuz-master

comparison paper/chapter/introduction.tex @ 26:657784b3bae1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add slide
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Sat, 30 Jan 2021 19:42:45 +0900
parents d9c29dddf64f
children af160f988ac8
comparison
equal deleted inserted replaced
25:d9c29dddf64f 26:657784b3bae1
35 他の形式手法にモデル検査がある。 35 他の形式手法にモデル検査がある。
36 モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。 36 モデル検査は実際に動作するコードですべての可能な実行の組み合わせを実行し検証する方法である。
37 例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。 37 例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。
38 モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。 38 モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。
39 OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。 39 OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。
40 しかしOSの処理は膨大であり、 様々な関数呼び出しや非決定的な処理、 並行処理などが発生する。 40 しかしOSの処理は膨大である。
41 モデル検査を行う場合でも、やみくもにOSのすべての処理を検査するのは難しい。 41 すべての存在可能な状態を数え上げるモデル検査では状態爆発が問題となる。
42 モデル検査自体が巨大な状態の検証を行うため、 状態を有限に制限したり抽象化を行う必要がある。 42 状態を有限に制限したり抽象化を行う必要がある。
43 43
44 44
45 OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。 45 OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。
46 その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。 46 その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。
47 OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。 47 OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。
52 証明を行う対象の計算は、 その意味が大きく別けられる。 52 証明を行う対象の計算は、 その意味が大きく別けられる。
53 OSやプログラムの動作においては本来したい計算がまず存在する。 53 OSやプログラムの動作においては本来したい計算がまず存在する。
54 これはプログラマが通常プログラミングするものである。 54 これはプログラマが通常プログラミングするものである。
55 それ以外にデータをメモリに保存するためにメモリのアロケーションをする処理や、メモリから値を持ってくる処理が入る。 55 それ以外にデータをメモリに保存するためにメモリのアロケーションをする処理や、メモリから値を持ってくる処理が入る。
56 メモリのほかにCPUの資源管理なども必要となる。 56 メモリのほかにCPUの資源管理なども必要となる。
57 さらにオブジェクト型の整合性の為にキャストなどの型変換が必要となる場合もある。 57 ユーザーレベルから見ると、データの読み込みなどは資源へのアクセスが必要であるため、システムコールを呼ぶ必要がある。
58 システムコール自体もメタ計算である。
58 ユーザーが本来やりたい計算以外に、資源管理などのこれら計算を行う上でやらなければならない計算が存在する。 59 ユーザーが本来やりたい計算以外に、資源管理などのこれら計算を行う上でやらなければならない計算が存在する。
59 前者の計算をノーマルレベルの計算と呼び、後者をメタレベルの計算と呼ぶ。 60 前者の計算をノーマルレベルの計算と呼び、後者をメタレベルの計算と呼ぶ。
60 プログラムの整合性の検証はメタレベルの計算と考えられる。 61 ノーマルレベルの計算を確実に行う為には、メタレベルの計算が重要となる。
62
63
64 プログラムの整合性の検証はメタレベルの計算で行いたい。
61 ユーザーが実装したノーマルレベルの計算に対応するメタレベルの計算を、自由にメタレベルの計算で証明したい。 65 ユーザーが実装したノーマルレベルの計算に対応するメタレベルの計算を、自由にメタレベルの計算で証明したい。
62 またメタレベルで検証ががすでにされたプログラムがあった場合、都度実行ユーザーの環境で検証が行われるとパフォーマンスに問題が発生する。 66 またメタレベルで検証ががすでにされたプログラムがあった場合、都度実行ユーザーの環境で検証が行われるとパフォーマンスに問題が発生する。
63 この場合はメタレベルの計算を検証をするもの、しないものと切り替えられる柔軟なAPIが必要となる。 67 この場合はメタレベルの計算を検証をするもの、しないものと切り替えられる柔軟なAPIが必要となる。
64 メタレベルの計算をノーマルレベルの計算と同等にプログラミングできると、動作するコードに対して様々なアプローチが掛けられる。 68 メタレベルの計算をノーマルレベルの計算と同等にプログラミングできると、動作するコードに対して様々なアプローチが掛けられる。
65 この為にはノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。 69 この為にはノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。