著者

北浜 優子 北嶋 曉 岡野 浩三 谷口 健一 キタハマ ユウコ キタジマ アキラ オカノ コウゾウ タニグチ ケンイチ 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%ほど作業時間がかかるものの効果的であることが確かめられた.

著者

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

出版者

電子情報通信学会

雑誌

電子情報通信学会論文誌. 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倍程度であること,等の結果より,本設計法および処理系の有効性が確かめられた.

著者

新井 凪 鈴木 彦文 小形 真平 岡野 浩三

雑誌

研究報告インターネットと運用技術(IOT) (ISSN:21888787)

巻号頁・発行日

vol.2021-IOT-55, no.1, pp.1-8, 2021-08-30

---

ネットワークの構築や構成変更において,その作業手順書を作成する開発者の負担が高いという問題がある.そのため従来から,ネットワーク機器設定コマンド(機器設定コマンド)からなるネットワーク機器設定手順(機器設定手順)を含んだ作業手順書を作成支援する方法が提案されてきた.しかし,多種多様なネットワーク構成に対応しやすい拡張性の高い方法は未だ確立されていない.その方法の確立に向けて本研究では,ネットワーク構成の設計を表す拡張性の高い厳密な仕様記法を確立し,この記法に準拠した設計仕様に基づいて作業手順書を自動生成する手法の確立を目的とする.本稿では,変更前後のネットワーク構成における設計仕様間の差分(変更差分)に基づき変更分の機器設定手順を自動生成する方法に焦点を当て,手法を検討した結果を報告する.また,小規模なネットワークの構成変更を事例として提案手法を適用した結果,期待された構成に変更できる機器設定手順が得られたことを確認した.

著者

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

出版者

情報処理学会

雑誌

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

巻号頁・発行日

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

参考文献数

14

被引用文献数

4

---

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

著者

柴田 直樹 岡野 浩三 谷口 健一 シバタ ナオキ オカノ コウゾウ タニグチ ケンイチ 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整数変数程度の規模のシステムであれば数秒程度(最悪時で数分程度)で検証できることが確かめられた.