Mercurial > hg > Papers > 2008 > atsuki-master

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/resume/Makefile	Wed Feb 20 03:18:06 2008 +0900
@@ -0,0 +1,72 @@
+MAKE=make -f Makefile
+LATEX=platex
+DVIPS=dvips
+DVIPDFM=dvipdfmx
+
+
+MAIN_TARGET=master_resume
+PS_SUFFIX=.ps
+PDF_SUFFIX=.pdf
+
+.SUFFIXES: .tex .dvi
+
+dvi:
+	@echo "========== MAKE DVI file ($(MAIN_TARGET).dvi) =========="
+	$(LATEX) $(MAIN_TARGET)
+
+final:
+	@echo "========== PUBLISHING =========="
+	@echo "\t first..."
+	$(LATEX) $(MAIN_TARGET) > /dev/null
+	@echo "\t second..."
+	$(LATEX) $(MAIN_TARGET) > /dev/null
+
+ps: final
+	@echo "========== GENERATE PostScript (PS) =========="
+	$(DVIPS) $(MAIN_TARGET)
+
+pdf: final
+	@echo "========== GENERATE PDF file =========="
+	$(DVIPDFM) $(MAIN_TARGET)
+
+clean:
+	@echo "remove $(MAIN_TARGET)*{aux,log,toc,lof,lot,blg,bbl,ilg,dvi,ps,pdf,out}"
+	@if [ -f $(MAIN_TARGET).aux ];\
+		then $(RM) $(MAIN_TARGET).aux;\
+	fi
+	@if [ -f $(MAIN_TARGET).log ];\
+		then $(RM) $(MAIN_TARGET).log;\
+	fi
+	@if [ -f $(MAIN_TARGET).toc ];\
+		then $(RM) $(MAIN_TARGET).toc;\
+	fi
+	@if [ -f $(MAIN_TARGET).lof ];\
+		then $(RM) $(MAIN_TARGET).lof;\
+	fi
+	@if [ -f $(MAIN_TARGET).lot ];\
+		then $(RM) $(MAIN_TARGET).lot;\
+	fi
+	@if [ -f $(MAIN_TARGET).blg ];\
+		then $(RM) $(MAIN_TARGET).blg;\
+	fi
+	@if [ -f $(MAIN_TARGET).bbl ];\
+		then $(RM) $(MAIN_TARGET).bbl;\
+	fi
+	@if [ -f $(MAIN_TARGET).ilg ];\
+		then $(RM) $(MAIN_TARGET).ilg;\
+	fi
+	@if [ -f $(MAIN_TARGET).dvi ];\
+		then $(RM) $(MAIN_TARGET).dvi;\
+	fi
+	@if [ -f $(MAIN_TARGET).ps ];\
+		then $(RM) $(MAIN_TARGET).ps;\
+	fi
+	@if [ -f $(MAIN_TARGET).pdf ];\
+		then $(RM) $(MAIN_TARGET).pdf;\
+	fi
+	@if [ -f $(MAIN_TARGET).out ];\
+		then $(RM) $(MAIN_TARGET).out;\
+	fi
+
+veryclean: clean
+	find ./ -name \*~  -exec rm -f {} \;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/resume/README	Wed Feb 20 03:18:06 2008 +0900
@@ -0,0 +1,40 @@
+修士最終発表予稿 用 スタイルファイル ver. 1.0.2
+
+Style-file for Proceedings of Master's Final Presentation
+  at Department of Information Engineering, University of the Ryukyus
+
+* ディレクトリの中身
+ README			...	このファイル
+ master_proc.sty	...	スタイルファイル
+ sample.tex		...	サンプルファイル
+
+* 仕様
+
+ 修士発表予稿のためのスタイルファイルです．予稿は，
+
+| 予稿仕様：
+|   A4用紙2枚、ダブル・カラム
+|   1ページ目（上マージン15mm, 下マージン20mm, 左マージン10mm, 右マージン20mm）
+|   2ページ目（上マージン15mm, 下マージン20mm, 左マージン20mm, 右マージン10mm）
+|   1ページ目ヘッダー部分に、学籍番号、氏名、指導教官名を記入する。
+
+ という仕様に基づいて作成しています．
+
+* 利用方法
+
+ 指定時にプリアンブルに
+ \documentclass[twocolumn, a4j, twoside]{jarticle}
+ \usepackage{master_proc}
+
+ \jtitle{和文タイトル}		%和文タイトル
+ \etitle{Title in English}	%英文タイトル
+ \author{氏名}	%著者名
+ \studentid{999999Z}	%学籍番号
+ \teacher{指導教官名}	%指導教官
+
+ を指定し，\begin{document} 直後に \maketitle してください．
+
+
+ 後はサンプルファイルを参照．
+
+--Ryuji GUSHIKEN
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/resume/master_proc.sty	Wed Feb 20 03:18:06 2008 +0900
@@ -0,0 +1,185 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%
+%%  Style-file for Proceedings of Master's Final Presentation
+%%    at Department of Information Engineering, University of the Ryukyus
+%%
+%%
+%%  ChangeLog:
+%%    version 1.0.1
+%%
+%%    Thu Feb 22 2001 Ryuji GUSHIKEN <ryuji@ads.ie.u-ryukyu.ac.jp>
+%%	* font size was make small under the thebibliography-environment
+%%    Thu Feb 22 2001 Ryuji GUSHIKEN <ryuji@ads.ie.u-ryukyu.ac.jp>
+%%	* modified *section parameters
+%%    Sun Feb 18 2001 Ryuji GUSHIKEN <ryuji@ads.ie.u-ryukyu.ac.jp>
+%%	* first release
+%%
+%%
+%%  USAGE:
+%%
+%%\documentclass[twocolumn, a4j, twoside]{jarticle}
+%%\usepackage{master_proc}
+%%
+%%\jtitle{修士論文最終発表用予稿作成テスト}		%和文タイトル
+%%\etitle{Test for Proc of Master's Final Presentation}	%英文タイトル
+%%\author{琉球 太郎}	%著者名
+%%\studentid{999999Z}	%学籍番号
+%%\teacher{先生 様々}	%指導教官
+%%
+%%\begin{document}
+%%  \maketitle
+%%  \section{はじめに}
+%%    はじめに，あいうえお．
+%%  \section{研究内容}
+%%    つぎに，かきくけこ．
+%%    \subsection{提案手法}
+%%      さしすせそ．
+%%    \subsection{アルゴリズム}
+%%      たちつてと(図~\ref{fig::test})．
+%%
+%%    \begin{figure}[b]
+%%      \begin{center}
+%%        \begin{minipage}{.2\textwidth}
+%%          \fbox{図図図図図図図図図図}
+%%	  図図図図図図図図図図図図図図図図
+%%	  図図図図図図図図図図図図図図図図
+%%	  図図図図図図図図図図図図図図図図
+%%        \end{minipage}
+%%      \end{center}
+%%      \caption{図のテスト}
+%%      \label{fig::test}
+%%    \end{figure}
+%%
+%%  \section{計算機実験}
+%%    そして，なにぬねの．
+%%    \subsection{実験手法}
+%%      はひふへほ．
+%%    \subsection{実験結果}
+%%      まみむめも(表~\ref{tbl::test})．
+%%
+%%    \begin{table}[tb]
+%%      \begin{center}
+%%        \caption{表のテスト}
+%%        \label{tbl::test}
+%%        \begin{tabular}{|c|}\hline
+%%          表表表表表表表表表表表表表表。\\\hline
+%%          表表表表表表表表表表表表表表。\\\hline
+%%          表表表表表表表表表表表表表表。\\\hline
+%%        \end{tabular}
+%%      \end{center}
+%%    \end{table}
+%%
+%%  \section{まとめ}
+%%    やゆよ\cite{last}．
+%%
+%%  \begin{thebibliography}{9}
+%%    \bibitem{last} わゐうゑを，''テストテスト,'' 2001.
+%%  \end{thebibliography}
+%%\end{document}
+%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\hoffset -1in \addtolength{\hoffset}{0mm}
+\voffset -1in \addtolength{\voffset}{15mm}
+\oddsidemargin 10mm
+\evensidemargin 20mm
+\topmargin 0mm
+\headheight 0mm
+\headsep 0mm
+\textheight 260mm %295-(15+20)mm
+\textwidth 180mm %odd-> 210-(10+20) : even->  210-(20+10)
+\marginparsep 0mm
+\marginparwidth 0mm
+\footskip \headsep
+
+\pagestyle{empty}
+
+%和文タイトル
+\def\jetitle{}
+\def\jtitle#1{\gdef\@title{#1}}
+%英文タイトル
+\def\@etitle{}
+\def\etitle#1{\gdef\@etitle{#1}}
+%学籍番号
+\def\@studentid{}
+\def\studentid#1{\gdef\@studentid{#1}}
+%指導教官
+\def\@teacher{}
+\def\teacher#1{\gdef\@teacher{#1}}
+\def\teacherlabel{指導教官:}
+
+\def\maketitle{%\par%
+  \begingroup
+    \if@twocolumn
+      \twocolumn[\@maketitle]
+    \else\newpage
+      \global\@topnum\z@\@maketitle \fi
+  \endgroup}
+
+\def\@maketitle{\newpage
+  \thispagestyle{empty}
+  \let\footnote\thanks
+  \begin{center}%
+    \begin{tabular*}{\textwidth}{cc}
+     \multicolumn{2}{c}{%
+       \parbox{\textwidth}{\center\LARGE \@title}}\\
+     \multicolumn{2}{c}{%
+       \parbox{\textwidth}{\center\Large \@etitle}}\\
+     \multicolumn{2}{c}{\rule{0pt}{10pt}}\\
+     \parbox[b]{.45\textwidth}{\center%
+ 	{\large\@studentid\hskip 1zw\@author}}&
+     \parbox[b]{.45\textwidth}{\center%
+ 	{\large\teacherlabel\hskip 1zw\@teacher}}\\
+    \end{tabular*}
+  \end{center}\vskip 5mm}
+
+% 章の見出し
+% 第4,5引き数はそれぞれ見出しの上下の空白の量である．
+% \@startsectionの第4引き数を負にすると見出しの後インデントしない．
+% 　　　〃　　　　第5引き数を負にすると見出しの後改行しない．
+% 　　　〃　　　　第6引き数は見出しフォントの指定
+\def\section{\@startsection {section}{1}{\z@}%
+	  {2ex plus 1ex minus .5ex}%
+	  {.3ex plus 1ex minus .3ex}%
+	{\large\bf}}
+\def\subsection{\@startsection{subsection}{2}{\z@}%
+	  {1ex plus 1ex minus .5ex}%
+	  {.1ex plus 1ex minus .3ex}%
+		{\normalsize\bf}}
+\def\subsubsection{\@startsection{subsubsection}{3}{\z@}{1.25ex plus
+ 1ex minus .2ex}{1.0ex plus .2ex}{\normalsize\bf}}
+\def\paragraph{\@startsection
+ {paragraph}{4}{\z@}{1.25ex plus 1ex minus .2ex}{-1em}{\normalsize\bf}}
+\def\subparagraph{\@startsection
+ {subparagraph}{4}{\parindent}{1.25ex plus 1ex minus
+ .2ex}{-1em}{\normalsize\bf}}
+
+\renewenvironment{thebibliography}[1]
+{\section*{\refname\@mkboth{\refname}{\refname}}%
+   \list{\small\@biblabel{\@arabic\c@enumiv}}%
+        {\settowidth\labelwidth{\@biblabel{#1}}%
+         \leftmargin\labelwidth
+         \advance\leftmargin\labelsep
+         \@openbib@code
+         \usecounter{enumiv}%
+         \let\p@enumiv\@empty
+         \renewcommand\theenumiv{\@arabic\c@enumiv}%
+	\setlength{\topsep}{10pt}%
+	\setlength{\itemsep}{1.5pt}%
+	\setlength{\parsep}{1.5mm}}
+   \sloppy
+   \clubpenalty4000
+   \@clubpenalty\clubpenalty
+   \widowpenalty4000%
+   \sfcode`\.\@m}
+  {\def\@noitemerr
+    {\@latex@warning{Empty `thebibliography' environment}}%
+   \endlist}
+\let\@openbib@code\@empty
+
+\def\bibitem{\small\@ifnextchar[\@lbibitem\@bibitem}
+\def\@lbibitem[#1]#2{\item[\@biblabel{#1}\hfill]\if@filesw
+      {\let\protect\noexpand
+       \immediate
+       \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+\def\@bibitem#1{\item\if@filesw \immediate\write\@auxout
+       {\string\bibcite{#1}{\the\value{\@listctr}}}\fi\ignorespaces}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/resume/master_resume.tex	Wed Feb 20 03:18:06 2008 +0900
@@ -0,0 +1,47 @@
+\documentclass[twocolumn, a4j, twoside]{jarticle}
+\usepackage{master_proc}
+\usepackage[dvips]{graphicx}
+
+% dvipdfm を使って PDF ファイルに日本語の栞をつける
+% \usepackage[dvipdfm]{color}
+% \usepackage[dvipdfm,bookmarks=true,bookmarksnumbered=true,%
+% bookmarkstype=toc]{hyperref}
+
+\jtitle{線形時相論理によるContinuation based Cプログラムの検証}		%和文タイトル
+\etitle{Verification of Continuation based C Program using Linear-time Temporal Logic}	%英文タイトル
+\author{下地 篤樹}	%著者名
+\studentid{068507B}	%学籍番号
+\teacher{河野 真治}	%指導教官
+
+\begin{document}
+\maketitle
+\section{はじめに}
+リアルタイムプログラムや並列プログラムのような非決定性を含むプログラムは、
+逐次型のプログラムに有効な二分法などによるデバッグ手法ではデバッグすることが
+困難である。
+そのため、非決定性を含むプログラムに対して有効なデバッグ手法や検証手法の
+確立が重要な課題となっている。
+
+そこで、本研究では、Continuation based C(CbC)言語による実装と
+その実装に対する検証手法を提案している。
+CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。
+そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。
+また、CbCで記述されたプログラムは状態遷移記述になるという性質がある。
+
+本研究は、CbCプログラムが状態遷移記述になることに着目し、
+状態遷移記述に対して有効である、タブロー法による状態の展開を行い、
+状態を展開する際に、線形時相論理も同時に展開することにより検証を行う。
+検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用さ
+れる。
+
+{\small
+\begin{thebibliography}{9}
+    \bibitem{bib:jssst2000kono}
+	河野真治. ``継続を持つCの下位言語によるシステム記述''.
+	日本ソフトウェア科学会第17回大会, 2000.
+    \bibitem{bib:sigos2007}
+	下地篤樹, 河野真治. ``線形時相論理によるContinuation based Cプログラムの検証''.
+	情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), April, 2007.
+\end{thebibliography}
+}
+\end{document}