\chapter{序論}
\pagenumbering{arabic}

%% 問題提起
%% 解決案の提示
%% 研究目標
%% 本論文の各章の概要

\section{研究の背景と目的}
リアルタイムプログラムや並列プログラムのような非決定性を含むプログラムは、
逐次型のプログラムに有効な二分法などによるデバッグ手法ではデバッグすることが
困難である。
そのため、非決定性を含むプログラムに対して有効なデバッグ手法や検証手法の
確立が重要な課題となっている。
%近年、ソフトウェアは大規模かつ複雑なものが増えてきている。
%そのため、設計および実装段階において誤りが生じる可能性が高くなってきており、
%設計または実装されたシステムに誤りがないことを保証するための論理設計や検証手法および
%デバッグ手法の確立が重要な課題となっている。

%ソフトウェアの信頼性を高めるため、現在はテスト手法による開発が中心となっている。
%しかし、ソフトウェアの規模の拡大や複雑化により、
%テスト手法では時間やコストがかかってしまう。

その課題の解決案として本研究では、Continuation based C(CbC)言語
による実装とその実装に対する検証手法を提案している。
CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
また、CbCで記述されたプログラムは状態遷移記述になるという性質がある。

本研究は、CbCプログラムが状態遷移記述になることに着目し、
状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
状態を展開する際に、線形時相論理も同時に展開することにより検証を行う。
検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用される。

\section{論文の構成}
第\ref{chapter2}章ではCbCの概要を説明し、
CbCプログラムの検証に必要となるタブロー法および、
線形時相論理について述べる。
また、検証に関連して他の検証ツールの概要を説明する。

第\ref{chapter3}章では、CbCプログラムのタブロー展開の手法およびその実装について説明する。
そして、線形時相論理によるCbCプログラムの検証の手法とその実装について述べる。

第\ref{chapter4}章では、実装したプログラムの評価を行い、それについて考察する。
また、他の検証ツールとの比較を行う。

第\ref{chapter5}章で本稿のまとめを述べる。