著者

北浜 優子 北嶋 曉 岡野 浩三 谷口 健一 キタハマ ユウコ キタジマ アキラ オカノ コウゾウ タニグチ ケンイチ Kitahama Yuko Kitajima Akira Okano Kozo Taniguchi Kenichi

出版者

情報処理学会

雑誌

情報処理学会論文誌 (ISSN:03875806)

巻号頁・発行日

vol.41, no.11, pp.3114-3121, 2000-11-15

---

形式的手法の設計導入教育への適用の有用性を調べるために,大阪大学基礎工学部情報科学科3年次学生のCPU設計実験において,(i)我々の研究グループで作成した検証システムを用いて設計の正しさを形式的に証明する設計手法(新手法),(ii)慎重な見直しや波形シミュレーションなどで設計の正しさを確認する設計手法(従来手法),の2つのコースを設けて,その2つのコース間で作業時間と設計したCPUにおける誤りの有無について2カ年にわたって比較を行った.定められた中間レポート提出期限までに誤りのないCPUを設計した学生は,従来手法コースでは42人中0人,新手法コースでは42人中41人であった.従来手法コースでは提出期限後に,教官が誤りを指摘して学生が設計を修正する期間を設け,この期間に19人が誤りのないCPUを設計した.中間レポート提出期限までに費やした全作業時間の平均は新手法43時間に比べて従来手法のほうが13時間ほど短かった.以上より,あらかじめ定められた期限までに正しいCPUを設計するためには,新手法は30%ほど作業時間がかかるものの効果的であることが確かめられた.

著者

北道 淳司 森岡 澄夫 東野 輝夫 谷口 健一

雑誌

全国大会講演論文集

巻号頁・発行日

vol.47, pp.123-124, 1993-09-27

---

ハードウェア記述言語では,複数の動作の並列実行を自然に記述できるものが多い.しかし,複数の動作が同じレジスタ,バス,端子等に異なるデータを転送する(データ代入の衝突)かどうかを判断することは難しい.高信頼という観点からは,データ代入の衝突が起きないことを保証し,その記述から高位合成することが望ましい.本論文では,2.において,同期式順序回路を対象とし,複数動作が実行される順序回路の一モデルを示し,そのモデル上でのデータ代入の衝突を定義する,3.において,衝突が起きないことを検証するアルゴリズムを与える.

著者

岡野 浩三 北道 淳司 東野 輝夫 谷口 健一

出版者

電子情報通信学会

雑誌

電子情報通信学会論文誌. D-I, 情報・システム, I-コンピュータ = The transactions of the Institute of Electronics, Information and Communication Engineers (ISSN:09151915)

巻号頁・発行日

vol.76, no.7, pp.354-363, 1993-07-25

参考文献数

9

被引用文献数

4

---

本論文では代数的手法による順序機械型プログラムの階層的設計法について提案する.我々の階層的設計法では要求仕様から実現プログラムまで同一の詳細化法に基づいて段階的に順次詳細化していく.各レベルでは,そのレベルでの関数,処理の性質等の要求記述が行われ,そのレベルで閉じた記述になっている.我々は,プログラム設計技法の共通問題として提供された在庫管理問題に対し本手法を適用し,他の文献では見られなかった入出力関係のみを指定した要求記述から,5段階にわたって逐次詳細化し,プログラムを開発した.本論文では記述の概略と共に,要求記述や詳細化の際に一般的に生じる問題点,解決法を述べ,また,他の方法論との比較も行っている.「拡張射影」と呼ばれる単純な枠組で最上位の満たすべき入出力関係を記述できること,記述は完全に階層的であること,各レベルの要求記述はいわゆるオーバスペックにならないように必要なことのみ記述していること,各レベルの要求記述に抜けがないよう記述スタイルを工夫していること,正しさの形式的な証明が可能であったこと,実現プログラムの実行時間はCプログラムのそれのたかだか2倍程度であること,等の結果より,本設計法および処理系の有効性が確かめられた.

著者

岡野 浩三 今城 広志 東野 輝夫 谷口健一

出版者

情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.34, no.6, pp.1290-1301, 1993-06-15

参考文献数

14

被引用文献数

4

---

分散システム全体の要求仕様から要求仕様通りに動作する各ノードの動作仕様(ざのようなタイミングでどのノードとどのような同期用メッセージやレジスタ値を交換しながら自ノードの動作を実行したり、自ノードのレジスタ値を更新していくべきかを記述したもの)を自動生成できることが望ましい。そこで、本論文ではレジスタを持つ拡張有限状態機械(EFSM)としてモデル化された分散システム全体の要求仕様から、要求仕様通りに動作する各ノードの動作仕様(EFSM)を自動生成するためのアルゴリズムを提案する。このモデルでは、非決定性の動作が記述できる。また、入カと状態だけでなくその時点のレジスタ値に依存して次の状態や次のレジスタ値を定めることができる。各レジスタは分散システムのリソースを表すと考える。どのノードに各リソースを配置するかは設計者が決める。同一リソースを複数ノードに分散配置してもよい。作成した自動生成アルゴリズムでは、与えられた要求仕様とゲートや、リソースの配置情報から各ノードの動作仕様を自動生成する。導出は要求仕様の各状態遷移を、選択動作の通知、レジスタ値の転送、レジスタ値の更新、更新終了の通知などの一連の動作の系列で置き換えることにより実現し、0?1線形計画問題の解法を用いて、その際のノード間のメッセージ交換の総数をできるだけ少なくしている。

著者

寺島 芳樹 安本 慶一 東野 輝夫 安倍 広多 松浦 敏雄 谷口 健一

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.42, no.2, pp.116-125, 2001-02-15

参考文献数

13

---

本論文では,種々の機能拡張に柔軟に対応できるQoS制御機構の実装法を提案し,SMILへの適用例を示す.提案手法では,仕様記述言語E-LOTOSのサブクラス(時間拡張LOTOSと呼ぶ)を中間言語として用いる.QoS制御機能は,システムを動画,音声の再生動作などを記述した主プロセスと,メディアスケーリング,メディア同期など追加したい機能のみを記述した制約プロセスとで構成し,それらを並列に同期実行させるという,制約指向スタイルを利用して実現する.またSMILに動的メディアスケーリング,メディア同期の精度指定の機構を追加したQOS-SMILを定義し,実装方法の適用例として示す.QOS-SMIL記述は対応する時間拡張LOTOS仕様に変換され,我々が開発している時間拡張LOTOSコンパイラを用いて実行される.いくつかの実験結果から,提案手法はQoS制御機能の開発コストに優れ,実行効率の点でも十分な性能を持っていることを確かめた.In this paper, we propose a flexible implementation technique forQoS control mechanisms and apply it to SMIL language.In the proposed technique, we use a subclass of E-LOTOS (calledreal-time LOTOS).We implement QoS control mechanisms using the constraint orientedstyle where a system is composed of a main process(e.g., video/audio playback) and several constraint processes (e.g.,media scaling, inter-media synchronization and so on). Usingthe multi-way synchronization mechanism of real-timeLOTOS, those processes run in parallel satisfying the specifiedconstraints.We define QOS-SMIL as an example extension of SMILwhere it has dynamic media scalingand explicit inter-media synchronization amongobjects, and show the applicability of our implementation technique.QOS-SMIL documents are converted to executable programs with ourreal-time LOTOS compiler. Through some experiments, we have confirmedthat the proposed technique has some advantages w.r.t. developmentcost for QoS control mechanisms and the derived programs haverelatively good performance for practical use.

著者

深田 敦史 鍛 忠司 東野 輝夫 谷口 健一 森 将豪

出版者

一般社団法人情報処理学会

雑誌

情報処理学会論文誌 (ISSN:18827764)

巻号頁・発行日

vol.39, no.8, pp.2519-2527, 1998-08-15

---

本論文では,入力を奪い合いながら並行に動作するDFSM群(DFSMsの直積マシン)としてモデル化される通信プロトコルのあるサブクラスに対して,DFSM群の状態と遷移の数の和に比例する程度のコストで効率良く適合性試験を行うための1つの手法を提案する.提案する方法では,まず,Wp法を用いて単独に各DFSMの試験を行う場合に用いる特性集合の和集合をシステム全体(DFSM群)の試験を行うための特性集合とする.入力を奪いあう場合,与えられた各特性系列に対して正しく反応を返す可能性のある状態対は複数存在する可能性がある.このため,各DFSMの1つの状態sの存在を確認するために,まず一定の条件を満たすW集合を構成する.次にその状態sを含む適切な状態組を1つ選び,その状態組に対する特性系列の反応をチェックすることにより状態sの存在を確認する.In this paper,we propose an effective conformance testing method for a subclass of protocols modeled as a set of DFSMs.The cost in the proposed testing method is only proportional to the sum of the numbers of states and transitions in a given set of DFSMs.In our method,we find a characterization set for each DFSM,which is used to test the DFSM alone in Wpmethod,and the union of the characterization sets is used as a characterization set for the total system.For a set of DFSMs with common inputs,there may exist two or more tuples of states that have correct responses against a given characterization set.So,in order to identify each state s in a DFSM,we find a characterization set with some specific properties.Then,we select a suitable tuple of states containing the state s,and identify the state s by checking their response to the characterization set.

著者

鍛 忠司 東野 輝夫 谷口 健一

雑誌

情報処理学会研究報告グループウェアとネットワークサービス(GN)

巻号頁・発行日

vol.1996, no.12, pp.19-24, 1996-01-25

---

通信プロトコルに対する適合性試験は通信システムの信頼性を高めるために有効である,従来,適合性試験系列の生成に関する研究の多くは単一の有限状態機械(S)によってモデル化されるソフトウェアを対象としている.しかし,複数のチャネルを持つ通信プロトコルなどでは,一つのチャネルの制御部を一つの決定性FSM(FS)でモデル化し,システム全体を入力を奪い合いながら並行に動作するDFSM群(FSMsの直積マシン)としてモデル化することが自然である.このようなシステムは全体としてもとのDFSM群の状態数の積に比例する状態を持つ非決定性FSM(FS)になる.このため,通常のNFSMに対する試験法を用いた場合,試験系列長がもとのDFSM群の状態数の積に比例するオーダーになるという問題点があった.本稿では,そのような入力を奪い合いながら並行に動作する複数のDFSM群としてモデル化されるような通信プロトコルのある部分クラスに対して,DFSM群の状態数の和に比例する程度のコストで効率よく適合性試験を行えるようにするための一つの手法を提案する,提案する手法では,まず,W?法を用いて単独に各DFSMの試験を行う場合に用いる先行系列の集合からシステム全体の試験を行うための先行系列の集合を生成する.また,各DFSMに対する特性集合の和集合をシステム全体の試験を行うための特性集合とする.次に,与えられた各特性系列に対して正しく反応を返す可能性のある状態対をすべて列挙し,その関係を表す制約式を生成する.これらの制約式を満たす解(状態の組)が仕様として与えられたDFSM群の状態対のみならば,与えられた先行系列の集合と特性集合に対して正しい反応を示す実装は仕様のDFSM群と等価であることが保証される.Conformance testing for communication protocols is useful for developing a highly reliable communication systems. Many researches have been done for test generation of the software modeled as a single finite-state machine (FSM). However, it is natural that the protocol with several channels is considered as a couple of DFSMs each of which controls a channel and competes with the others for common inputs. For this model, the existing methods have a problem that the derived test suite is proportional to the product of the numbers of states of DFSMs. In this paper, we propose an effective method of conformance testing for a subclass of protocols modeled as those couples of DFSMs. In our method, we find a state cover set for each DFSM, which is used to test the DFSM alone in W-method, and derive a state cover set for the total system from those sets. The characterization set for the total system is the union of those for the DFSMs. Then, we construct constraints representing the relation among tuples of states that have correct responses against the characterization set. If these constraints have only one solution, we guarantee that an IUT modeled as a couple of DFSMs which has correct responses against the state cover and characterization set is equivalent to the given specification.

著者

柴田 直樹 岡野 浩三 谷口 健一 シバタ ナオキ オカノ コウゾウ タニグチ ケンイチ Shibata Naoki Okano Kozo Taniguchi Kenichi

出版者

電子情報通信学会

雑誌

電子情報通信学会論文誌D (ISSN:09151915)

巻号頁・発行日

vol.J84-, no.7, pp.999-1008, 2001-07-01

---

加算をもつ有理数の理論(有理数変数,有理数定数,+,-,=,<∧, ∨, ∀, ∃からなる理論)の上の閉論理式(RP文)の真偽判定ルーチンは通信プロトコルのテスト,ハードウェアのタイミング検証などに利用できる.筆者らは以前,計算幾何学の手法を利用し,時間計算量を改善したRP文真偽判定アルゴリズムを提案した.本論文では,まずそのアルゴリズムに対する凹多面体併合を用いた高速化法について述べる.次に,その手法を実装した真偽判定ルーチンをMC68030バス上で非同期バスマスタ転送を行う時間オートマトンの適合性試験系列生成に適用し,評価した結果について述べる.高速化により,比較的簡単な時間制約をもつ時間オートマトンの実行可能性判定の例に対し,実際の検証で現れる変数の数が16個,不等式の数が20個程度のRP文をCPU時間数秒程度(Pentium III 600 MHz)で判定できるようになった.

著者

竹中 崇 岡野 浩三 東野 輝夫 谷口 健一

出版者

一般社団法人電子情報通信学会

雑誌

電子情報通信学会論文誌. D-I, 情報・システム, I-情報処理 (ISSN:09151915)

巻号頁・発行日

vol.87, no.4, pp.462-470, 2004-04-01

参考文献数

10

---

整数変数をもつ有限状態機械(FSM/int)に対する記号モデル検査法を提案する.入力値を保持する変数の値は次に同一遷移で新たな値が読み込まれるまで変更されない,などの制約を満たす,与えられたFSM/intに対し,整数変数をもつCTL式を満たすか否かをこの記号検査アルゴリズムは判定する.この記号モデル検査アルゴリズムを実装し,ブラックジャックディーラ回路とバケット多重化プロトコルに適用した.そして,100状態,10整数変数程度の規模のシステムであれば数秒程度(最悪時で数分程度)で検証できることが確かめられた.

著者

森岡 澄夫 柴田 直樹 東野 輝夫 谷口 健一

出版者

一般社団法人電子情報通信学会

雑誌

電子情報通信学会技術研究報告. VLD, VLSI設計技術

巻号頁・発行日

vol.96, no.299, pp.49-56, 1996-10-18

被引用文献数

5

---

加算器, 乗算器, ALUなど, 算術演算を行う組み合わせ論理回路が, そのワードレベル仕様F (整数上の論理式として書かれた入出力関係の記述) を正しく実現している事を, プレスブルガー文真偽判定手続きを用いて自動証明する方法と, 証明例について述べる. 証明は, いわゆるビットレベル検証 (各回路モジュールM_jごと, そのワードレベル仕様F_jがゲートレベルで正しく実現されていることの証明) とワードレベル検証 (各M_jの接続関係および各ワードレベル仕様F_jのもとで, Fが満たされることの証明) に分けて行う. 乗算など, プレスブルガー算術で直接扱えない演算を行う回路についても, その演算に関して数学的に成り立つ性質等を仮定することにより, 証明できる場合がある. 本手法の特徴は, 幾つかの工夫を行ったプレスブルガー真偽判定ルーチンを用いることにより, 各モジュールの演算ビット長 n が増えても, 回路中のモジュールの数や組合せ方が同じで, かつ仕様記述のサイズが n 依存していなければ, ワードレベル検証にかかる時間がほとんど増加しないことである. 例えば n ビット乗算器から 2n ビット乗算器を構成した場合のワードレベル検証を, 2分程度のCPU時間で行えた. ビットレベル検証についても, 演算ビット長が4ビット程度であれば, 例えば加減算・論理演算を行うALU (74382) について6分程度のCPU時間で行えた.

著者

北嶋 暁 森岡 澄夫 島谷 肇 東野 輝夫 谷口 健一

出版者

一般社団法人電子情報通信学会

雑誌

電子情報通信学会論文誌. D-I, 情報・システム, I-コンピュータ (ISSN:09151915)

巻号頁・発行日

vol.79, no.12, pp.1017-1029, 1996-12-25

参考文献数

15

被引用文献数

4

---

教育用CPU KUE-CHIP2を,各命令の意味を記述した要求仕様からRTレベルまで段階的に設計し,それをSFL記述に自動変換してハードウェア合成系パルテノンを用いて回路を得た.そして,その設計が正しいことを代数的手法に基づいた証明支援系を用いて完全に自動で証明した.自動で証明できた理由は,CPUでは,要求仕様も含め,各レベルの仕様が共通の基本関数(算術・論理演算,メモリの入出力)を用いて記述できる,CPUの正しさの証明では1命令ごとに正しく動作することを調べればよく,かつ1命令の実行では繰返しループを含まない,また,我々の開発した証明支援系では,項書換え,場合分け,整数上の論理式の恒真性判定などを一定の手順で自動実行する,扱う式の大きさが増大するのに対処した工夫をしている,などである.証明作業は,記述誤りに伴う再証明も含め2週間程度で行えた.CPUの命令数が増えても証明のための計算時間はそれに比例する程度ですむので,本実験の結果より,単一制御部をもつ非パイプラインCPUについては,本論文の手法により,その正しさの証明を,現実的な時間で自動で行うことが可能であると言える.