# HG changeset patch
# User ikkun <ikkun@cr.ie.u-ryukyu.ac.jp>
# Date 1588362950 -32400
# Node ID 965bbb629a1b7f733cb7562ae0344ab9982a08b6
# Parent  3bece84a4022963aa228c6d6ee0787ccfc958714
written intoro

diff -r 3bece84a4022 -r 965bbb629a1b paper/ikkun-sigos.pdf
Binary file paper/ikkun-sigos.pdf has changed
diff -r 3bece84a4022 -r 965bbb629a1b paper/ikkun-sigos.tex
--- a/paper/ikkun-sigos.tex	Fri May 01 23:57:08 2020 +0900
+++ b/paper/ikkun-sigos.tex	Sat May 02 04:55:50 2020 +0900
@@ -34,7 +34,7 @@
 \affiliate{3}{琉球大学工学部}
 
 
-\author{東恩納　琢偉}{Takui Higashionna}{1}[ikkun@cr.ie.u-ryukyu.ac.jp
+\author{東恩納　琢偉}{Takui Higashionna}{1}[ikkun@cr.ie.u-ryukyu.ac.jp]
 \author{奥田　光希}{Okuda Kouki}{2}[Koki.okuda@cr.ie.u-ryukyu.ac.jp]
 \author{河野　真治}{Shinji kono}{3}[kono@ie.u-ryukyu.ac.jp]
 
@@ -63,15 +63,23 @@
 \maketitle
 
 %1
-\section{背景}
- 
+\section{プログラムの信頼性}
+リアルタイムプログラムや並列プログラムのような非決定生を含むプログラムは、逐次型のプログラムに有効な二分法などによるうデバック手法ではデバックする事が困難である。そのため、非決定生を含むプログラムに対して有効なデバック手法や検証手法の確立が重要な課題となっている。本研究ではモデル検査を用いる事でプログラムの信頼性を保証する手法として、GearsOSにおけるモデル検査手法について提案する。
+モデル検査はプログラムの設計から導出されたモデルが形式仕様を満たすかを検証することで信頼性を保証する、しかしプログラムの規模が大きくなると導出されるモデルの状態数が爆発的に増えるため、それら全てを検証する手法は好ましくない、そのため記録する状態を抽象化、または限定する方法について考察する。
+
+\section{Gears OS}
+モデル検査はプログラムの状態記述を線形時相論理の論理式の形式で記述し検証する手法が一般的である。
+本研究室で開発しているGeasOS は CbC で記述されており、プログラムの処理が記述された code gear と変数などのデータを格納する data gear によって構成され、Code Gear 間の遷移にはgoto を用いて遷移する。このため CbC による記述は状態遷移記述になる性質がある。
+また goto による遷移は大域変数を持たない遷移であるため、遷移前の処理に囚われず遷移先を自由に変更する事が可能である。
+Gears OS はこの性質を利用して処理の間に meta Code Gear を入れることでメタ計算を途中で行う事ができる。
+
 
 
 
 
 
 %2
-\section{モデル検査}
+\section{}