| 講演名 | 2004/5/7 整数制約論理のための二分決定グラフの拡張データ構造とそれに対するアルゴリズムの提案 北道 淳司, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本稿では,ある整数制約論理の処理のためのデータ構造およびその上での論理演算に関する基本アルゴリズムを提案する.例えば,リアルタイムシステムの設計では,システムのイベントの発生などを時刻で表し,システムの仕様はイベント発生時刻が満たすべき制約からなる論理式として表現することができる.具体的に得られた設計仕様が要求仕様を満たすかどうかを形式的に検証するには,時刻を表す変数を含む論理式を処理し,要求仕様を満足するかどうかを検証する必要がある.本研究では,イベント発生時刻を整数変数で表現し,一つの論理項に最大2つの整数変数を含むような項からなる論理式を取り扱う.そのような論理式を表現するデータ構造を提案し,そのデータ構造に対する論理演算処理について述べる.これらの基本処理を組み合わせることにより,モデル検査アルゴリズムなどの検証アルゴリズムを実現することができる. |
| 抄録(英) | We propose new data structure and algorithms for an integer restricted arithmetic. In this integer restricted arithmetic, which consists of logical and integer variables and operators, we can describe specifications of real time systems. Proposed data structure is an extended BDD (Binary Decision Diagram), which is one of methods expressing Boolean functions. We also describe some algorithms for proposed data structure. |
| キーワード(和) | 形式的検証 / 制約論理 / 二分決定グラフ |
| キーワード(英) | Formal Verification / Integer Restricted Arithmetic / BDD |
| 資料番号 | SS2004-5 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2004/5/7(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 整数制約論理のための二分決定グラフの拡張データ構造とそれに対するアルゴリズムの提案 |
| サブタイトル（和） | |
| タイトル（英） | Proposal of Data Structure based on BDDs(Binary Decision Diagrams) and Algorithms for an Integer Restricted Arithmetic |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 形式的検証 / Formal Verification |
| キーワード(2)（和/英） | 制約論理 / Integer Restricted Arithmetic |
| キーワード(3)（和/英） | 二分決定グラフ / BDD |
| 第 1 著者 氏名（和/英） | 北道 淳司 / Junji KITAMICHI |
| 第 1 著者 所属（和/英） | 会津大学 School of Computer Science and Engineering, The University of Aidu |
| 発表年月日 | 2004/5/7 |
| 資料番号 | SS2004-5 |
| 巻番号（vol） | vol.104 |
| 号番号（no） | 47 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |