|
1
|
1 \chapter*{要旨}
|
|
16
|
2
|
|
8
|
3 開発手法の一つとして，形式手法というものがある．
|
|
|
4 形式手法とはプログラムの仕様を形式化，つまり数学的な記述を行い，
|
|
16
|
5 書いたプログラムがそれを満たしているか検証を行う開発手法である．
|
|
8
|
6 代表的な形式の検証手法として，定理証明やモデル検査が挙げられる．
|
|
|
7
|
|
16
|
8 形式手法で開発したプログラムは数学的に正しいことが証明されている.
|
|
8
|
9 そのため高い安全性が必要とされる鉄道や電力などのインフラ分野に使用されている．
|
|
16
|
10 一見完璧な手法であるように思えるが欠点として，形式化や検証が複雑なため膨大なコストを要する．
|
|
|
11 シンプルな実装であれば仕様の形式化が容易に行えるが，そうであれば形式手法を使用する利点が薄くなる．
|
|
8
|
12
|
|
16
|
13 そのため，他のプログラミング言語と比べて検証に適している Gears Agda を使用する．
|
|
|
14 Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を
|
|
|
15 取り入れた記法で記述された定理証明支援器 Agda のことである．
|
|
8
|
16
|
|
|
17 定理証明によるプログラムの検証は一般的に難易度が高いが，
|
|
15
|
18 Gears Agda では検証をプログラム単位に分割することができ，比較的容易に検証を行えるようになっている．
|
|
8
|
19
|
|
15
|
20 先行研究では implies を用いて Hoare Logic での定理証明を行っていた.
|
|
16
|
21 しかし、それでは記述が長く複雑になっていた.
|
|
|
22 そこで今回は Invariant というプログラムの不変条件を新たに取り入れた.これを検証しながら実行をすることで,Hoare Logic を用いた定理証明を比較的簡単に行えるようになった.
|
|
13
|
23
|
|
16
|
24 また，定理証明では並列処理の検証は困難である。出現する状態を一度全て出してからそれらの検証を行わないといけないためである。
|
|
8
|
25 そのため，もう一つの代表的な検証手法であるモデル検査を Gears Agda にて行えるようにした．
|
|
|
26
|
|
16
|
27 これらのことから，本論文では Gears Agda の定理証明とモデル検査での検証手法について述べる。
|
|
1
|
28
|
|
|
29 \chapter*{Abstract}
|
|
14
|
30 One of the development methods is called formal methods.
|
|
|
31 Formal methods formalize the specification of a program, i.e., describe it mathematically, and verify that the written program satisfies the specification.
|
|
|
32 The typical formal verification methods include theorem proving and model checking.
|
|
|
33 Theorem proving and model checking are typical formal verification methods.
|
|
|
34
|
|
|
35 Programs developed by formal methods are proven to be mathematically correct.
|
|
|
36 For this reason, they are used in infrastructure fields such as railroads and electric power, where high safety is required.
|
|
|
37 However, the drawback of this seemingly perfect method is that it is extremely costly.
|
|
|
38 Formalization of specifications is easy for simple implementations, but then it is not necessary to use formal methods.
|
|
|
39
|
|
|
40 For this reason, we use Gears Agda, which is more suitable for verification than other programming languages.
|
|
|
41 Gears Agda is a programming language written in a notation that incorporates the concept of Continuation based C (CbC), which is being developed in our laboratory.
|
|
|
42 Gears Agda is an Agda written in a notation that incorporates the concept of Continuation based C (CbC), which is being developed in our laboratory.
|
|
|
43
|
|
|
44 Verification of programs by theorem proving is generally difficult.
|
|
15
|
45 Gears Agda can be divided into program units, making verification relatively easy.
|
|
14
|
46
|
|
|
47 In previous research, implies were used for theorem proving in Hoare Logic.
|
|
|
48 However, this made the description long and complicated.
|
|
|
49 Therefore, in this study, we introduced a new program invariant called Invariant. By verifying the invariant condition while executing the program, theorem proving using Hoare Logic became relatively easy.
|
|
|
50
|
|
|
51 In addition, verification of concurrency is difficult in theorem proving.
|
|
|
52 Therefore, we made it possible to perform model checking, another typical verification method, in Gears Agda.
|
|
|
53
|
|
|
54 Based on the above, this paper describes the theorem proving and model checking verification methods of Gears Agda.
|
