時制論理に基づく仕様記述とそのデバッグ環境
スポンサーリンク
概要
- 論文の詳細を見る
並列プログラムの実行過程の解明や知能ロボットの行動計画生成問題は時間的関係を含んだ問題として定式化され,その方法として時制命題論理(PTL:Propositional Temporal Logic)による解決が試みられている.このようなPTLをベースとした具体的システムでは,論理式を形式的な仕様とみなし,仕様を満たすような手順系列を自動的に生成することができる.また,PTLで書かれた仕様が正しければ,その結果得られる手順系列も正しいことが保証されている.しかし,PTLによって記述された仕様(論理式)自体に誤り,不足がある場合は当然のことながらその結果も誤りとなる.ところが,結果の検証,デバッグはいまだに人手で行なわれている.バグとしては,(1)記述ミス(スペルミス),(2)きつい仕様(無駄な制約),(3)仕様が記述不足(制約が不足),を考える.(1)は原子命題や論理記号の記述ミスである.(2)では,無駄な制約のために,結果として得られるモデル集合(M)がユーザーが実行したいもの(U)に比べ小さなもの,すなわち,M⊆Uとなる.従って,MをUによって検証すれば必ず矛盾が発生し,その矛盾点を追跡することでバグを発見することができる.ところが,(3)は必ずしも検証過程で矛盾を引き起こすとは限らない.なぜなら,M⊇Uだからである.この場合,むしろ,不足している仕様が何であるかをユーザーから与えられるモデルから生成する機能が必要となる.そこで,(3)以外の二つのバグを同定する方法について述べる.まず,ここで対象とするPTLとその決定手続きであるタブロー法について解説し,PTL式のバグが何であるのかを定義する.次にユーザーモデルに基づいたバグの発見アルゴリズムについて詳述する.
- 一般社団法人情報処理学会の論文
- 1989-03-15
著者
関連論文
- CSTソリューションコンペティション2007及び2008の総括(ペトリネット,離散事象システム,一般)
- AI-2-1 CSTソリューションコンペティション2008 : 総括(AI-2.CSTソリューションコンペティション2008:表彰式・シンポジウム,ソサイエティ企画)
- AK-2-3 マルチカーエレベータ群管理アルゴリズムに関する研究動向 : CSTソリューションコンペティション2007の活動を通じて(AK-2.基礎・境界分野の研究最前線,ソサイエティ特別企画,ソサイエティ企画)
- CSTソリューションコンペティション2007 : 評価実験の詳細報告(コンカレントシステム,離散事象システム,ハイブリッドシステム,及び一般)
- AI-1-5 CSTソリューションコンペティション2007(総括)(AI-1. CSTソリューションコンペティション2007:表彰式・シンポジウム,依頼シンポジウム,ソサイエティ企画)
- AS-3-4 CSTソリューションコンペティション2010の概要 : マルチカーエレベータの最適制御(AS-3.コンカレントシステム理論の最近の発展とその応用,シンポジウムセッション)
- A-12-8 CSTソリューションコンペティション2007 : 課題と評価ツール(A-12.コンカレント工学,一般講演)
- AP-2-5 CSTソリューションコンペティション2007(概要)(AP-2.コンカレント技術研究の方向性,パネル討論,ソサイエティ企画)
- 三段階ネット指向ソフトウェア設計法
- 超逐次プログラミング : 高信頼並行プログラムの新しい開発手法の提案
- TA-2-2 高水準ペトリネットによるソフトウェア設計法(TA-2. 高水準ペトリネットのシステムとソフトウェア開発への応用,チュートリアル講演)
- 会話によるプログラミング : 動的並列オブジェクト指向言語の提案
- 代数的仕様と時制論理によるリアルタイムSAとオブジェクト指向設計の融合手法
- 仕様記述過程モデル化のための実験と分析
- 時相論理とその応用 (<特集>非標準論理とその応用)
- 時制論理に基づく仕様記述とそのデバッグ環境
- 知的プログラミングシステム (AI技術)
- 並列プログラムの知的プログラミング支援システムMENDELS(3) : 時制論理からの同期部の自動生成
- 並列プログラムの知的プログラミング支援システムMENDELS(2) : 部品再利用による本体部の生成
- 並列プログラムの知的プログラミング支援システムMENDELS(1) : システム構成
- ライフサイクル計画方法論の構築(第2報) : 製品ライフサイクル計画手法の提案
- ペトリネットは便利な道具
- 仕様獲得と知識獲得 1.仕様獲得 vs. 知識獲得 (<特集>仕様獲得と知識獲得)
- 階層的問題解決システムにおける抽象階層の決定方法
- 仕様獲得支援システム:K-SCORE(3) : 仕様精錬部の構成とその機能
- 仕様獲得支援システム:K-SCORE(2) : 仕様構成部の構成とその機能
- 仕様獲得支援システム:K-SCORE(1) : システム概要と仕様実行部
- 仕様獲得支援システムの開発 : 仕様デバッガの試作
- 89-31 自動計画生成におけるインヘリタンス
- 89-8 計画と解釈のデバッグ理論
- 複数ビューに基づくシステム仕様化過程の分析
- 情報システムの企画・計画技術
- 不確実な電力事業環境下における発電設備投資計画法
- 不確実な環境下における発電設備の投資計画の一手法(電力のOR)
- 5ZC-6 並行プログラムに関するテスト・デバッグ方式
- 組込み制御用ソフトウェア次世代テスト・デバッグシステム
- 高水準ペトリネットによるソフトウェア開発方法論
- 製造業のサービス事業化の課題と設計支援技術
- 時制論理とペトリネット(AIの推論とOR)
- AP-4-3 コンカレント技術ロードマッピングへの招待(AP-4.コンカレント技術の現在・過去・未来,パネル討論,ソサイエティ企画)
- ネット指向戦略シナリオ・プランニング手法の提案
- 複合ビューポイントに基づく仕様化プロセスの分析
- 製品ライフサイクルでの高信頼化技術の動向 : 仕様と実装と環境のギャップを監視・検出・修正するヘルスマネジメント
- 製品ライフサイクルでの高信頼化技術の動向 : 仕様と実装と環境のギャップを監視・検出・修正するヘルスマネジメント
- 製造業のサービスイノベーションのための知識処理技術(サービスイノベーションとAI)
- コンカレント工学における技術ロードマッピングに関する考察(コンカレントシステム, 一般)
- 3. 制御用プログラムの試験 (<特集>「並行処理におけるプログラム試験」)
- 離散事象システムの網羅的シミュレーション
- シ-ケンス制御プログラムの検証技術
- 特集「仕様獲得と知識獲得 : ソフトウェアシステムの視点から」の編集にあたって
- 様相論理による並行プログラムの積重ね式検証法
- 通信制御ソフトウェアの時相論理による検証 : CCITT勧告X.25の検証
- 大規模有向グラフの効率的記憶法 : アニーリング法を利用したラベル付け
- Robin Milner 著, "Communication and Concurrency", Prentice Hall International Series in Computer Science, B5判, 260p., \3,790, 1989
- 89-3 ストリームのための自動プログラミングII : プログラム変換による実現法
- CSTソリューションコンペティション2010 : マルチカーエレベータの最適制御(CSTソリューションコンペティション2010,コンカレントシステム及び一般)
- コンカレント工学研究会の活動を振り返って : 歴代委員長からのメッセージ(一般,コンカレントシステム及び一般)
- 3. 応用分野の最前線 3.4 制御分野における自動プログラミング (自動プログラミング)
- 推論型システム記述言語 MENDEL
- 1-D-7 医療・介護サービスにおける音声つぶやきコミュニケーションによる連携業務のモデル化(特別セッション サービスサイエンス)
- 仮想フィールドを用いた看護・介護サービスにおける音声つぶやきコミュニケーションの評価実験について (システム数理と応用)
- 看護・介護サービスのための時空間を越えたコラボレーション支援
- 看護・介護サービスにおける複雑なプロセスのモデル化にむけて(グラフ,ペトリネット,ニューラルネット,及び一般)
- 看護・介護サービスにおける複雑なプロセスのモデル化にむけて(グラフ,ペトリネット,ニューラルネット,及び一般)
- 音声つぶやきによる看護・介護の時空間コミュニケーション : 情報スーパーバイザ制御の提案
- 音声つぶやきによる看護・介護の時空間コミュニケーション : 情報スーパーバイザ制御の提案
- 音声つぶやきによる看護・介護の時空間コミュニケーション : 情報スーパーバイザ制御の提案
- 音声つぶやきによる看護・介護の時空間コミュニケーション : 情報スーパーバイザ制御の提案
- 仮想フィールドを用いた看護・介護サービスにおける音声つぶやきコミュニケーションの評価実験について
- 看護・介護サービスにおける複雑なプロセスのモデル化にむけて
- 看護・介護サービスにおける複雑なプロセスのモデル化にむけて
- A-12-13 節電と経済活性化を両立させるサービス設計(A-12.システム数理と応用,一般セッション)
- 音声つぶやきによる看護・介護の時空間コラボレーション支援 : システムの概要と試行評価結果
- 音声つぶやきによる看護・介護の時空間コラボレーション支援 : システムの概要と試行評価結果
- イベントログに基づいた行動型サービスの分析(システムと信号処理及び一般)
- イベントログに基づいた行動型サービスの分析(システムと信号処理及び一般)
- イベントログに基づいた行動型サービスの分析(システムと信号処理及び一般)
- イベントログに基づいた行動型サービスの分析(システムと信号処理及び一般)