非単調命題時間論理とその形式的仕様記述への応用
スポンサーリンク
概要
- 論文の詳細を見る
本論文は,形式的仕様記述に使用するための非単調命題時間理論について述べたものである.時間理論は,並列システムや通信プロトコルといった動的システムを形式的に記述するには有用であるが,実際,人間がシステムの諸性質を検証できるほど完全に記述するのは難しい.というのは,人間は常識に基づいた暗黙的推論を行っているため,システムの細部にまでわたって時間理論で完全に記述することが難しいからである.本論部では「記述されていない状態遷移は一切起こらない」,「共有変数の値は更新されたことが示されない限り保持される」という2つの暗黙的推論が行えるような非単調な命題時間論理を提案する.この論理は,通常の線形時間論理に既存のtemporalオペレータの機能を損なうことなく,McDermottの手法に基づいて,ある時刻における論理式の無矛盾性を表す様相オペレータを追加したものである.その意味は,証明可能性演算子の不動点を用いることによって与える.さらに,Tableau法に基づく証明手続きを与え,実際の仕様記述例と仕様の諸性質の推論例についても述べる.ユーザが仕様として記述した論理式の集合に,上記の暗黙的推論を行うための論理式が追加され,推論が行われる.追加される論理式は,あらかじめ用意れたスキーマと仕様として記述された論理式の構文とによって自動的に生成される.
- 一般社団法人情報処理学会の論文
- 1987-06-15
著者
関連論文
- CAiSE'06参加報告
- CAiSE' 06参加報告
- ゴール指向要求分析のためのドメインオントロジの利用法(ソフトウェア開発とオントロジー,プロジェクト管理とモニタリング,一般)
- 要求分析のためのドメインオントロジ構築支援
- ドメインオントロジを用いた要求獲得支援ツールの実現
- 榎本肇先生を偲んで(追悼抄)
- アスペクト概念を利用したゴール指向要求獲得法
- 要求仕様と再利用可能な実現構造の振る舞いの差分検出に基づく要求分析(オブジェクト指向,言語設計(学生セッション))
- モデル駆動型開発におけるモデルメトリックスの定義手法
- 第1回アジア太平洋ソフトウェア工学国際会議(APSEC'94)報告
- 第1回アジア太平洋ソフトウェア工学国際会議(APSEC'94)報告
- 第1回アジア太平洋ソフトウェア工学国際会議(APSEC'94)報告
- ユースケース記述に対するフレームワーク利用法の導出(アーキテクチャ・フレームワーク(学生セッション))
- 非同期型のコミュニケーションを用いた共同作業における阻害要因の分析
- 静的解析と動的解析を用いたデザインパターン検出手法
- UMLで記述したモデルの構成管理支援法(要求工学)
- デザインパターンのオブジェクト指向モデル化と支援ツールへの応用(ソフトウェアシステム)
- デザインパターンのオブジェクト指向モデル化と支援ツールへの応用
- フレームワークの要求仕様に対する適合性の評価手法
- グラフ変換を用いたUMLモデルのリファクタリング支援
- デザインパターンのモデル化と適用支援ツール
- ソフトウェアパターンの変換に基づくソフトウェア開発
- フレームワークに基づいた変更支援法について
- ベイジアンネットワークを用いたソフトウェア実装技術の選択支援
- 要求獲得におけるシソーラスの効果・効用について
- シソーラスを用いた要求分析法
- ASE2004参加報告
- 要求分析のためのシソーラス作成支援
- サマーワークショップ・イン・立山 開催報告
- 仕様記述過程モデル化のための実験と分析
- PAORE : パッケージ指向の要求獲得プロセス
- インタビューによる要求抽出作業を誘導するシステムの実現方法
- インタビューによる要求抽出作業を誘導するシステムの実現方法
- 要求工学における人工知能技術(知能ソフトウェア工学〔第4回〕)
- 6 要求仕様の品質特性(要求工学)
- ゴールグラフからのフィーチャモデル導出(要求,アーキテクチャ(学生セッション))
- 座談会 人間の知能と機械の知能 : 1986年9月6日 於:北海道大学
- CAiSE'06参加報告
- CAiSE'06参加報告
- 要求工学国際会議(RE'04)の開催を振り返って(要求工学・ドメイン分析)
- 振る舞いモデルを用いたフレームワーク利用支援ツール
- オブジェクト指向は本当に役立っているのか : ソフトウェア工学の立場およびソフトウェア科学の立場から
- オブジェクト指向は本当に役立っているのか : ソフトウェア工学の立場およびソフトウェア科学の立場から
- シソーラスを利用した要求獲得方法(THEOREE)
- 編集操作の分類に基づくソースコード差分の構造化
- コモンクライテリアをドメイン知識としたゴール指向セキュリティ要求獲得法
- 対面式会議を支援する計算機システムの評価実験
- 要求仕様作成会議の発話履歴を利用した仕様記述法の適用・評価
- ソフトウェアの要求獲得を支援する対面式会議システムに関する一考察
- 要求仕様作成会議の発話履歴を利用した仕様書の記述法
- 仕様作成会議の発話履歴と仕様書の構造に関する分析
- 仕様作成会議の発話履歴を用いて仕様書を作成する方法
- ウィンターワークショップin神戸報告
- ユースケース記述からの状態遷移モデル生成
- 特集「アジア・太平洋のソフトウェア技術」の編集にあたって (アジア・太平洋のソフトウェア技術)
- 方法論の構築支援ツール
- Expert System for Specification Process in Software Development System Pure TELL
- 自然言語仕様からモジュール構造を得る手法について
- 自然言語の語彙に基づいたオブジェクト指向仕様記述言語
- 自然言語に基づくソフトウェア部品の結合方式の考察
- 自然言語に基づいたソフトウェア設計プロセス
- 自然言語に基づく静的システムの仕様のプロトタイププログラムへの変換手法
- 自然言語と図を用いた仕様記述言語の構造化エディタの開発
- モデルチェッカを用いた要求仕様の法令準拠性の検査
- 要求分析・設計時における代替案選択のための意思決定法
- カラーペトリネットによるオブジェクト指向ソフトウェアのテストと解析方法
- カラーペトリネットによるオブジェクト指向ソフトウエアのテストと解析方法
- プロダクト統合のためのソフトウェア仕様化・設計法のモデル化手法の提案
- ソフトウェア仕様化/設計法のデータベースの試作
- デザインパターン検出のためのテストケース作成支援
- セマンティック要求工学
- 1.アジアにおけるソフトウェア工学 (アジア・太平洋のソフトウェア技術)
- 動的スライシングを用いた漸進的Feature Location手法
- ベイジアンネットワークを用いた実装プラットフォームの選択支援
- 属性つきゴール指向要求分析法の支援のための統合ツール
- 属性つきゴール指向要求分析法の支援のための統合ツール
- ドメインオントロジを用いた自然言語文書とソースコード間の追跡可能性の復元(オントロジ,教育(学生セッション))
- グラフ変換を用いたアーキテクチャ代替案選択の支援
- 仕様書とJavaソースコードの構造の類似性に基づく対応付け(アーキテクチャ・フレームワーク(学生セッション))
- 探索手法を用いたリファクタリング情報の抽出(学生セッション H_開発支援)
- UMLで記述したモデルの構成管理支援法(要求工学)
- フレームワークの要求仕様に対する適合性の評価手法
- フレームワークの要求仕様に対する適合性の評価手法
- ソフトウェアの仕様記述過程の分析(II)
- ソフトウェアの仕様記述過程の分析(I)
- ゴールグラフの品質向上支援ツールとその評価 (知能ソフトウェア工学)
- ICSE '96会議報告
- 第18回ソフトウェア工学国際会議報告
- ソフトウェアの実現段階における会議の分析
- アイコンシステムの開発
- ソフトウェアの設計段階における会議の分析
- 4+1ビューモデルにもとづくソフトウェアアーキテクチャの記述およびその評価法
- Automated Software Engineering 2005参加報告
- ゴール指向要求分析を用いたステークホルダの対立の検出(要求工学(学生セッション))
- ソフトウェアメトリクスの統合によるソースコード変更の選択(メトリクス(学生セッション))
- メトリクス値の変化の可視化によるプログラム変更の支援(メトリクス(学生セッション))
- シナリオとゴールに基づく要求分析におけるオントロジ活用法(ソフトウェア開発とオントロジー,プロジェクト管理とモニタリング,一般)
- 法律や規則に適合した要求の獲得支援
- ドメインオントロジを用いたゴール指向要求分析支援(学生セッション,大学のAI・企業のAI)
- ドメインオントロジを用いたゴール指向要求分析支援(学生セッション,大学のAI・企業のAI)