Mercurial > hg > Papers > 2018 > nozomi-master
comparison paper/abstract.tex @ 148:cf9c3be20362
add Alice abstract
| author | Nozomi Teruya <e125769@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 25 Jan 2018 18:15:48 +0900 |
| parents | 2e30ed0e2633 |
| children | d620f126a383 |
comparison
equal
deleted
inserted
replaced
| 147:d7b8a5d1252f | 148:cf9c3be20362 |
|---|---|
| 1 \begin{abstract} | 1 \begin{abstract} |
| 2 高い信頼性を持つソフトウェアを提供することは重要である。 | 2 スマートフォンやタブレット端末の普及率が増加している。 |
| 3 それには、ソフトウェアが期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。 | 3 それに伴いインターネット利用者数も増加しており、ネットワーク上のサービスには |
| 4 特に実際に動作するソフトウェアを検証や証明できるとなお良い。 | 4 、信頼性とスケーラビリティーが要求される。 |
| 5 本論文では 検証や証明に直接使用することができる言語として Continuation based C(CbC) 言語を用いる。 | 5 ここでいう信頼性とは、定められた環境下で安定して仕様に従った動作を行うことを |
| 6 指す。 | |
| 7 またスケーラビリティーとは、スケーラビリティとは、分散ソフトウェアに対して単純にノードを追加するだけで性能を線形的に上昇させることができる性質である。 | |
| 8 しかし、これらをもつ分散プログラムをユーザーが一から記述することは容易ではない。 | |
| 6 | 9 |
| 7 CbC上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法を提案し、メタ計算ライブラリ akasha として実装した。 | 10 これらの問題の解決のために、当研究室ではデータをData Segment、タスクをCode Segmentという単位で記述するプログラミング手法を導入した分散フレームワークAlice の開発を実現した。 |
| 8 akasha では赤黒木の仕様を、限定的な木の大きさの範囲内で検証した。 | 11 Data Segmentは整数や文字列や構造体などの基本的なデータの集まりである。 |
| 12 Code Segmentは入力となるData Segmentが全て揃ったら処理を開始し計算結果のData Segmentを出力するタスクである。 | |
| 9 | 13 |
| 10 木の大きさを制限せず実装が仕様を満たすことを示すには証明が必要である。 | 14 Aliceが実用的な分散アプリケーションを記述でき、仕様の変更を抑えた信頼性の高い拡 |
| 11 プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが知られている。 | 15 張を可能にするということは、水族館の例題やTreeVNCの例題から確認された。 |
| 12 本論文では依存型を持つ証明支援系 Agda を用いて証明を行なう。 | 16 しかし、AliceではAPI設計が直感的でなく、型の整合性がとれない問題があった。また、AliceにNAT越えの機能を実装しようとした際、Data Segment Managerが1つしか持てない |
| 13 部分型を用いてCbC の項を型付けすることで、CbC の形式的定義を型システムより相似的に得る。 | 17 たために拡張が困難であることが分かった。 |
| 14 これらの形式的定義を Agda によって記述し、Single Linked Stackの満たす性質を証明した。 | 18 |
| 19 本研究では、Aliceから得られた知見をもとに、分散フレームワークChristieの設計を行った。 | |
| 20 | |
| 21 | |
| 15 | 22 |
| 16 \end{abstract} | 23 \end{abstract} |
| 17 | 24 |
| 18 \begin{abstract_eng} | 25 \begin{abstract_eng} |
| 19 Proving highly reliable software is important. | |
| 20 One way is checking if the specification is satisfied or not, the other way is to prove the implementation satisfies the specification directly. | |
| 21 If we can check or prove actual implementations, it it much better. | |
| 22 In this paper, we use Continuation base C programming language (CbC) which can be used in both model checking and proof. | |
| 23 | |
| 24 We propose model checking method by enumerating bounded computational state in CbC code as a meta computation. | |
| 25 Akasha meta computation library makes it possible to check red-black tree algorithm within a bounded tree size. | |
| 26 | |
| 27 To assure the property for arbitrary size of trees, we need proof method. | |
| 28 Proofs in a program are known to correspond $\lambda$ calculus, which is a Curry-Howward Isomorphism. | |
| 29 We use dependently typed Agda proof assistance system. | |
| 30 Formal definitions of CbC are similarly defined by subtyped CbC terms using Agda. | |
| 31 We prove properties of Single Linked Stack using proposed formal definitions. | |
| 32 \end{abstract_eng} | 26 \end{abstract_eng} |
| 33 | 27 |