#""の中に名前を書いてください
author = "東恩納 琢偉"

#""の中に学籍番号を書いてください
user_id = "198592C"

#論文タイトル
title = "Gears OS でモデル検査を実現する手法について"

#論文タイトル(英語)
title_en = "Method for Realizing Model Checking in Gears OS"

#アブストラクト """の間に書いてください。
abstract = """
アプリケーションはテストと言われる方法を用いてバグを発見し修正することで信頼性を高める。しかしバグの再現性が低い場合には発見は困難になる。この際にはデバックを行うプログラマーの経験により予想した原因に基づいて１つ１つチェックをしていく必要がある。
モデル検査とは、検証したいアプリケーションの状態遷移記述を用いて行われ、特定の状態から遷移する全ての組み合わせに対して検査を行うことで信頼性を保証する。
当研究室ではアプリケーションやサービスの信頼性をOSの機能として保証することを目指し、 Gears OS という OS を開発しており、モデル検査による検証や、定理証明を用いる事での信頼性へのアプローチを行っている。
本研究では Gears OS における Dining Philosophers ploblem のモデル検査を行うことで Gears OS におけるモデル検査手法の確立し、DPP に適応させる。さらに Gears OS 上でのメタ計算による自身のモデル検査について研究する。

"""

#アブストラクト(英語) """の間に書いてください。
abstract_en = """
applications are made more reliable by finding and fixing bugs using a method called testing. However, if the reproducibility of the bugs is low, it becomes difficult to find them. In this case, it is necessary to check the bugs one by one based on the expected cause based on the experience of the programmer who does the debugging.
　Model checking is performed using the state transition description of the application to be verified, and the reliability is guaranteed by checking all combinations of transitions from a specific state.
　In our laboratory, we are developing an OS called Gears OS to guarantee the reliability of applications and services as an OS function, and are approaching reliability by using model checking and theorem proving.
In this research, we establish a model checking method for Gears OS by performing model checking of Dining Philosophers ploblem in Gears OS, and adapt it to DPP. In addition, we will study model checking by meta-computation on Gears OS.
"""

#卒論・修論のPDFのパス
#卒論がpapers/thesis.pdfだったら、thesis_pdf = "papers/thesis.pdf"
#修論がmaster_paper.pdfだったら、thesis_pdf = "master_paper.pdf"と書く

thesis_pdf = "master_paper.pdf"

#予稿のPDFのパス
#B4は必須
#preliminary_pdf = "preliminary.pdf"

#英語予稿のPDFのパス
#preliminary_en_pdf = "preliminary_en.pdf"



#ポスターのパス
#Googleスライドなどの場合は、URLでもよい
#poster_pdf = "poster.pdf"

#スライドのパス
#Googleスライドなどの場合は、URLでもよい
slide_path = "http://www.cr.ie.u-ryukyu.ac.jp/hg/Papers/2021/ikkun-master/raw-file/tip/presen/slide.html"

#自分の研究室の行の先頭の「#」を消してください

#supervisor = "ファイヤー和田研"
#supervisor = "吉田研"
#supervisor = "名嘉村研"
#supervisor = "姜研"
#supervisor = "宮里研"
#supervisor = "山田研"
#supervisor = "岡崎研"
supervisor = "河野研"
#supervisor = "當間研"
#supervisor = "赤嶺研"
#supervisor = "遠藤研"
#supervisor = "長山研"
#supervisor = "長田研"
#supervisor = "國田研"