Mercurial > hg > Papers > 2008 > atsuki-master
changeset 4:18753cb3c703
*** empty log message ***
author | atsuki |
---|---|
date | Wed, 13 Feb 2008 20:52:35 +0900 |
parents | 23fe35aec32b |
children | db0d95f0b2e0 |
files | paper/bibliography.tex paper/chapter2.tex |
diffstat | 2 files changed, 8 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/bibliography.tex Wed Feb 13 20:34:13 2008 +0900 +++ b/paper/bibliography.tex Wed Feb 13 20:52:35 2008 +0900 @@ -1,6 +1,9 @@ -%\chapter*{参考文献} -%\addcontentsline{toc}{chapter}{参考文献} +\begin{thebibliography}{99} + \bibitem{bib:spin} + ``Spin - Formal Verification''. + http://spinroot.com/spin/whatispin.html -\begin{thebibliography}{99} - + \bibitem{bib:javapathfinder} + ``Java PathFinder''. + http://javapathfinder.sourceforge.net/ \end{thebibliography}
--- a/paper/chapter2.tex Wed Feb 13 20:34:13 2008 +0900 +++ b/paper/chapter2.tex Wed Feb 13 20:52:35 2008 +0900 @@ -232,7 +232,7 @@ \subsection{SPINの概要} 有限状態遷移系に対する形式的検査手法としてモデル検査手法がある。 -その代表的なツールとしてSPINがある。 +その代表的なツールとしてSPIN\cite{bib:spin}がある。 SPINは、プログラム変換的な手法で検証するツールで、 検証対象をPROMELA(PROcess MEta LAnguage)という言語で記述し、