@techreport{oai:ipsj.ixsq.nii.ac.jp:00021134, author = {平野, 清美 and 宇佐美, 雅紀 and 藤倉, 俊幸 and Kiyomi, HIRANO and Masanori, USAMI and Toshiyuki, FUJIKURA}, issue = {52(2007-SE-156)}, month = {May}, note = {従来の形式仕様記述のレベルはデータ制約を扱うシミュレーションまでであったが,本研究によりモデル検査技術を利用することで検証レベルを上げることができたので報告する., This paper describes about the enhancement of the verification level of embedded software. Although the verification level of the conventional formal specification language is limited to a simulation, using model checking enhance the verification level.}, title = {モデル検査への事前条件・事後条件検証の導入}, year = {2007} }