Pat

J-GLOBAL ID：200903003109083830

ソフトウェア仕様の検証方法

Inventor： 佐藤 正和
Applicant, Patent owner： 株式会社エイ・ティ・アール通信システム研究所
Agent (1)： 深見 久郎 (外2名)
Gazette classification：公開公報
Application number (International application number)：1994135803
Publication number (International publication number)：1996006778
Application date： Jun. 17, 1994
Publication date： Jan. 12, 1996
Summary：

【要約】【目的】 複数プロセス間にわたる状態遷移規則を、変数を含む書換え型のプロダクションルールとして与え、特定の状態がある仕様によって与えられたシステムに出現するか否かを検証することができるようなソフトウェア仕様の検証方法を提供する。【構成】 ステップ1において準広域状態mの値が入力される。ステップ2において、可到達可能な準広域状態の集合である可到達状態集合の大きさを一定値にする。ステップ3において入力されたmの値によって決定された準広域状態SGm が可到達状態集合Ri に含まれるか否か判定される。ステップ4において、含まれる場合には可到達であると判定され、含まれない場合には非可到達であると判定される。

Claim (excerpt)：

n個の機能手段の状態の遷移規則が変数を含むプロダクションルールとして与えられるソフトウェア仕様において、前記n個の機能手段のうちm個の機能手段の特定状態が前記ソフトウェア仕様で決定されるシステムに現われるか否か検証するソフトウェア仕様の検証方法であって、前記mの値が与えられる第1のステップと、前記nの値を大きくし、前記m個の機能手段の選び得る状態のうちで前記システムに現われる状態の集合を一定値にする第2のステップと、前記一定値にされた集合に前記m個の機能手段の特定状態が含まれるか否かを判定する第3のステップと、判定結果に応じて、前記m個の機能手段の特定状態が前記システムに現われるか否かを判定する第4のステップとを含む、ソフトウェア仕様の検証方法。

IPC (4)：

G06F 9/06 530 ,  G06F 9/06 540 ,  H04L 29/14 ,  H04Q 3/545