Mercurial > hg > Papers > 2008 > atsuki-master
changeset 15:0ba2de3295b8
*** empty log message ***
author | atsuki |
---|---|
date | Mon, 18 Feb 2008 01:15:24 +0900 |
parents | 39242aece5fc |
children | 6bd5455a9335 |
files | paper/chapter1.tex |
diffstat | 1 files changed, 2 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/chapter1.tex Sun Feb 17 14:24:23 2008 +0900 +++ b/paper/chapter1.tex Mon Feb 18 01:15:24 2008 +0900 @@ -20,9 +20,9 @@ による実装とその実装に対する検証手法を提案している。 CbCは、C言語より下位でアセンブラより上位のプログラミング言語である。 そのため、C言語よりも細かく、アセンブラよりも高度な記述が可能であるという利点がある。 -また、CbCで記述されたプログラムは非決定性状態遷移記述と近い構造になるという性質がある。 +また、CbCで記述されたプログラムは決定性状態遷移記述と近い構造になるという性質がある。 -本研究は、CbCが非決定性状態遷移記述と相性の良い言語であることに着目し、 +本研究は、CbCが決定性状態遷移記述と相性の良い言語であることに着目し、 非決定性状態遷移記述に対して有効である、タブロー法による状態の展開を行い、 状態を展開する際に、線形時相論理も同時に展開することにより検証を行うことを目的としている。 検証において、時相論理はシステムの要求仕様を記述する方法として形式的検証で利用される。