LOTOS仕様の時間特性検証方法に関する一検討
スポンサーリンク
概要
- 論文の詳細を見る
筆者らはLOTOSを応用し,設計仕様の機械検証能力に特長を持つ通信ソフトウェア設計支援環境ITECS(Integrated Environment for high reliability Communication Software design and development)を現在開発している。ITECSはLOTOSで記述した仕様の時間特性を検証する機能Vegaを提供している。Vegaは実際の開発工程では、要求仕様に示されるイベントの順序関係がLOTOS仕様に正しく反映されているかを検証するために用いることが多い。本論文では、この検証作業を効率的に行う方法の一検討について述べる。
- 社団法人電子情報通信学会の論文
- 1995-03-27
著者
関連論文
- 通信ソフトウェア設計支援環境(ITECS)の評価
- 通信ソフトウエア設計支援環境:ITCES(4) : 仕様検証支援系(Verifier,vega)
- 仕様の段階的詳細化とグラフ表現に基づく統合型記述支援
- シミュレーション関係を用いた大規模システムの部分検証に関する考察
- 通信ソフトウエア設計支援環境 : ITECS(1):システム全体構成
- MSCとLOTOSによる通信システム設計支援システム
- 相互接続試験系列生成システム : TESGEN
- 相互運用性試験に対する試験系列生成方式の検討
- ITECSにおける仕様検証支援
- LOTOS仕様の時間特性検証方法に関する一検討