特許
J-GLOBAL ID：201103015787125051
ソフトウェア仕様の証明支援装置、及び証明支援方法
発明者：
,
,
出願人/特許権者：
代理人 (2件)：
井上 学
, 戸田 裕二
公報種別：公開公報
出願番号（国際出願番号）：特願2010-113811
公開番号（公開出願番号）：特開2011-242955
出願日： 2010年05月18日
公開日（公表日）： 2011年12月01日
要約：
【課題】ソフトウェア仕様の証明に失敗した場合に、修正候補の確認及び選択作業をせずに、ソフトウェア仕様を修正できるようにする【解決手段】ソフトウェア証明支援装置は、入力されたソフトウェア仕様からその不変条件候補一覧を抽出し、前記不変条件候補一覧から抽出した不変条件候補を前記ソフトウェア仕様から推論し、推論した不変条件候補を前記ソフトウェア仕様に追加することで、ソフトウェア仕様を修正する。【選択図】図1
請求項（抜粋）：
形式言語で記述されるソフトウェア仕様を証明するソフトウェア証明支援装置であって、
プロセッサ、及び記憶部を備え、
前記記憶部は、前記ソフトウェア仕様を証明するための証明方法と、前記ソフトウェア仕様から前記ソフトウェア仕様の性質を推論するための、前記証明規則とは異なる推論規則を格納し、
前記プロセッサは、
前記推論規則によって、前記ソフトウェア仕様から前記ソフトウェア仕様の性質を推論し、
推論した前記ソフトウェア仕様の性質を、前記ソフトウェア仕様の前提条件として前記ソフトウェア仕様に追加し、
前記証明方法によって、前記ソフトウェア仕様を証明する
ことを特徴とするソフトウェア証明支援装置。
IPC (1件)：
FI (1件)：
Fターム (2件)：
引用特許：
前のページに戻る
