著者

片山 卓也 島津 明 東条 敏 二木 厚吉 緒方 和博 有本 泰仁 落水 浩一郎 早坂 良

出版者

JAIST Press

巻号頁・発行日

vol.2, 2007-09

---

法令工学は,法令文書の作成や変更,法令実働化情報システムの構築を系統的に行うため,人工知能,言語処理,ソフトウェア工学の研究成果を使おうとする工学的アプローチであり,21 世紀COEプログラム「検証進化可能電子社会」の主要研究課題の一つである.安心な電子社会の実現には,電子社会の仕様書である法令を適切に作成し,それを施行する情報システムを正しく構築しなければならない.また,法令の改定に対しては,関係法令への変更伝播を整合的に行い,それを情報システムへの変更に矛盾なくつなげる必要がある.法令工学は,このような問題を工学的に解決することめざして,本COEで世界で初めて提案されたものである.現在,企業活動における法令尊守などが大きな社会問題として取り上げられているが,組織における規則の作成や尊守機構の設計なども法令工学の範疇に入ると考えられ,今後訪れる本格的な電子社会時代において,安心で公正な社会や組織の設計や実現に,法令工学はその基本技術を提供するものであると考えている.本書は,本COEにおける法令工学の研究活動を紹介するために書かれたものであるが,各章の著者は以下のようである.第1章 片山卓也 第2章 島津明 第3章 東条敏 第4章 二木厚吉,緒方和博,有本泰仁 第5章 落水浩一郎,早坂良

著者

原 光太朗 緒方 和博 中村 正樹 二木 厚吉

出版者

FIT(電子情報通信学会・情報処理学会)運営委員会

雑誌

情報科学技術フォーラム一般講演論文集

巻号頁・発行日

vol.3, no.1, pp.177-178, 2004-08-20

著者

緒方 和博

出版者

北陸先端科学技術大学院大学

雑誌

基盤研究(B)

巻号頁・発行日

2019-04-01

---

我々の生活を便利にするシステムは高信頼であるべきだ。さもなければ、多額の財産を失う等の多大な不便をこうむることになる。システムを高信頼にするために使うことのできる技術のひとつはモデル検査である。システムが期待される要件を満たすかどうかを自動で検証出来る。しかし、システムの到達可能状態空間が大きくなり過ぎてモデル検査不能になる問題が起こる。本研究計画では、到達可能状態空間を複数の部分空間に分割し、各々の部分空間でモデル検査を行えるようにすることでこの問題を緩和することを試みる。加えて、複数の部分空間に対するモデル検査を同時並列に実行することでモデル検査の効率化も試みる。

著者

二木 厚吉 緒方 和博 中村 正樹 Kokichi Futatsugi Kazuhiro Ogata Masaki Nakamura 北陸先端科学技術大学院大学情報科学研究科 北陸先端科学技術大学院大学情報科学研究科 北陸先端科学技術大学院大学情報科学研究科 Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST) Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST) Graduate School of Information Science Japan Advanced Institute of Science and Technology (JAIST)

出版者

日本ソフトウェア科学会

雑誌

コンピュータソフトウェア = Computer software (ISSN:02896540)

巻号頁・発行日

vol.25, no.2, pp.1-13, 2008-04-24

参考文献数

6

被引用文献数

3

---

CafeOBJ言語システムを用いた形式手法,すなわち形式仕様の作成法と検証法,を全6回にわたり解説する.CafeOBJ言語はOBJ言語を拡張した代数仕様言語であり,振舞仕様,書換仕様,パラメータ化仕様などが記述できる最先端の形式仕様言語である.CafeOBJ言語システムは,等式を書換規則として実行することで等式推論を健全にシミュレートすることができ,対話型検証システムとして利用出来る.第1回の今回は,「待ち行列を用いる相互排除プロトコル」を例題として,言語や検証法の細部に立ち入ることなく,CafeOBJ仕様の作成と検証が全体としてどのように行われるかを説明する.第2回以降では,言語の構文と意味(第2回),等式推論と項書換システム(第3回)について説明し,証明譜を用いた簡約のみに基づくCafeOBJの検証法(第4回)を解説する.さらに,認証プロトコル(第5回)と通信プロトコル(第6回)の2つの典型的な検証例も示すことで検証の技法についても解説する.The formal method, or the method for writing and verifying formal specifications, with the CafeOBJ language system is described in a series of six tutorials. The CafeOBJ language is a most advanced formal specification language which extents the OBJ language, and behavioral, rewriting, and parameterized specifications can be written in it. The CafeOBJ language system can simulate equational reasoning by executing equations as rewrite rules, and be used as an interactive verification system. This first tutorial presents an overview of the CafeOBJ formal method by using an example of "mutual exclusion protocol with a waiting queue" without getting into details of the language and the verification technique. In the following tutorials, the language and its semantics (2nd tutorial), equational reasoning and term rewriting systems (3rd tutorial) are presented, and the CafeOBJ's verification method with proof scores which only uses reductions (4th tutorial) is explained. Furthermore, CafeOBJ's verifications of an authentication protocol (5th tutorial) and a communication protocol (6th tutorial) are also presented, and several verification techniques are explained.

著者

二木 厚吉 緒方 和博 中村 正樹

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.25, no.2, pp.2_1-2_13, 2008 (Released:2008-06-30)

---

CafeOBJ言語システムを用いた形式手法,すなわち形式仕様の作成法と検証法,を全6回にわたり解説する.CafeOBJ言語はOBJ言語を拡張した代数仕様言語であり,振舞仕様,書換仕様,パラメータ化仕様などが記述できる最先端の形式仕様言語である.CafeOBJ言語システムは,等式を書換規則として実行することで等式推論を健全にシミュレートすることができ,対話型検証システムとして利用出来る.第1回の今回は,「待ち行列を用いる相互排除プロトコル」を例題として,言語や検証法の細部に立ち入ることなく,CafeOBJ仕様の作成と検証が全体としてどのように行われるかを説明する.第2回以降では,言語の構文と意味(第2回),等式推論と項書換システム(第3回)について説明し,証明譜を用いた簡約のみに基づくCafeOBJの検証法(第4回)を解説する.さらに,認証プロトコル(第5回)と通信プロトコル(第6回)の2つの典型的な検証例も示すことで検証の技法についても解説する.

著者

緒方 和博

雑誌

科学研究費補助金研究成果報告書

巻号頁・発行日

pp.1-5, 2009-04-10

---

証明支援系とモデル検査器を効果的に利用できるよう、定理証明向きのシステム仕様をモデル検査向きのシステム仕様に自動変換する方法を考案した。変換により、モデル検査向きのシステム仕様が大きくなりすぎて効果的にモデル検査ができなくなることを防ぐための工夫を行った。提案した変換方法の有効性を確認するため、電子商取引プロトコルiKPとMondexの検証実験に適用した。また、変換を支援する変換ツールの拡張性の高い実装方法も提案した。この実装方法では、複数の変換規則をモジュラーに組み入れることを可能にする。