著者

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

出版者

JAIST Press

巻号頁・発行日

vol.2, 2007-09

---

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

著者

片山 卓也

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.36, no.3, pp.3_33-3_46, 2019-07-25 (Released:2019-09-25)

---

国民年金法の述語論理による記述と定理自動証明システムZ3Pyによる検証に関するケーススタディついて述べた.法令の作成は伝統的に人手により行われて来たが,近年法令が大量に作られるようになり,その品質の維持には計算機科学,特にソフトウェア工学や人工知能で培われた技術を応用することが有効であると考えられる.本稿では,法令を意図した通りに正しく作る上で,法令の形式的記述と自動検証技術が有効であることを確認する目的で,国民年金法の基本的条文の述語論理による記述と,そのSMTソルバーZ3Pyによる検証を試行した結果を報告する.法令の文章上の複雑さは別にすると,その論理的深度は深くなく,このような方法が誤りの無い法令を作る上で有効な方法になり得ることが分かった.

著者

片山 卓也

出版者

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

雑誌

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス (ISSN:09135685)

巻号頁・発行日

vol.107, no.99, pp.13-16, 2007-06-14

被引用文献数

1

---

我々の社会は、非常に多数の相互に関連した法律により規定されている。それらは社会の組織や構造、目標や目的を記述すると同時に、組織における活動や手続きを定めており、われわれはその法律に従って社会活動を行っている。したがって、法律が適切に作られており、それが社会のなかで正しく運用されていることは、社会の安心性の基本である。これは、社会というシステムを考えたとき、法律がこのシステムの仕様の役割を果たしていることを意味している。本稿では、このような観点から、法律の作成および法律を実現する情報シメテムの構築に対して工学的アプローチを提案し、その研究課題などについて展望する。

著者

片山 卓也

出版者

JAIST Press

巻号頁・発行日

pp.1-146, 2021-12

---

国民年金法のような行政サービスに関する法令は,その内容は明確であり,文章上の見かけの複雑さの割には論理的深度は深くない.したがって,形式的手法によってその内容を記述することにより,可読性が高く,機械的なテストや分析が可能な法令記述が得られる可能性が高い.また,このような法令は我々の社会の制度的基盤であり,その法令実働化IT システムが我々の社会生活を 支えていることを考えると,法令に対する形式的技術の確立は重要である. 本書は,このような立場から行政サービスに関する法令を意図した通りに正しく作る上で,法令の形式的記述と自動検証技術の可能性を,国民年金法の基本的条文の述語論理による記述と定理自動証明器(SMT ソルバー)Z3Py による検証事例に基づいて述べたものである.近年の定理証明技術の進歩や計算機システムの高性能化により,このような技術は十分に実用化可能であるというのが本書の結論である.法令の度重なる改正に対応するため法令実働化ITシステムの内部構造劣化が進み,保守の困難性が社会的な問題となっているが,本書で述べる技術はこの問題に対する有力な解決法になると思われる. 本書は2部から構成されている. 第I部はこのような新しい法令作成方法論の原理的可能性を示すために書かれた,日本ソフトウェア科学会誌「コンピュータソフトウェア」36巻3号(2019)に掲載された論文をそのままの形で転載したものである. 被保険者の資格,年金の支給期間及び支払期月,併給の調整に関する3 つの典型的条文を通して,論理式化の方法やその構造化の方法等を示すと同時に,検証に必要なテストデータとしての年金原簿の扱いなどについて述べている.また,条文の誤りの定理証明システムによる検証例について述べている. 第II部は,第I部で述べた内容を事例の面から補強するために,そこで紹介した方法を国民年金法のより多くの条文へ適用した結果を詳細かつ具体的に述べたものであり,このような手法を広く実践する際の助けとなることを目的としたものである. 各条文ごとに,(1)条文の文章,(2)論理式記述,(3)検証スクリプトと検証結果,(4)それらの内容に関するメモを付加した.論理式記述は,パターン表現を用いてなるべく簡潔になるように心懸けたが,このようなパターンの定義などを基本用語定義集として纏めた.検証においてはテストデータとしての年金原簿が必要であるが,各条文の検証に必要な複数の年金原簿も纏めて収録した.最後に,日付けを抽象データとして扱った検証事例,実際の暦による日付け記述,論理式記述に基づく年金システムシミュレーターの構成の概略などを収録した.

著者

片山 卓也

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.36, no.3, pp.3_33-3_46, 2019

---

<p>国民年金法の述語論理による記述と定理自動証明システムZ3Pyによる検証に関するケーススタディついて述べた.法令の作成は伝統的に人手により行われて来たが,近年法令が大量に作られるようになり,その品質の維持には計算機科学,特にソフトウェア工学や人工知能で培われた技術を応用することが有効であると考えられる.本稿では,法令を意図した通りに正しく作る上で,法令の形式的記述と自動検証技術が有効であることを確認する目的で,国民年金法の基本的条文の述語論理による記述と,そのSMTソルバーZ3Pyによる検証を試行した結果を報告する.法令の文章上の複雑さは別にすると,その論理的深度は深くなく,このような方法が誤りの無い法令を作る上で有効な方法になり得ることが分かった.</p>

著者

田村 直良 片山 卓也

出版者

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

雑誌

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

巻号頁・発行日

vol.25, no.2, pp.260-267, 1984-03-15

---

本論文では双方向性階層的関数型プログラミングBi-HFPを提案する.HFPでは 一つの処理単位をモジュールによって表す.各モジュールは値の授受のために入力属性挫出力属性のリストをもつが この属性の値がある条件(結合条件)を満たしたときに 親モジュールをより簡単な処理を行う子モジュールに分割する.分割時には 親 子モジュール間の属性方程式(意味規則)に従ってさらにいくつかの属性値が決定される.Bi-HFPにおいてはHFPと同一な記述を 結合条件が満たされたときに子モジュールが親モジュールに統合されるというようにも拡張解釈する.Bi-HFPの記述例としてパーザについて述べる.われわれの方法では 扱う文脈自由文法の非終端記号をモジュールに 生成規則をモジュールの分割統合に対応させる.処理する入力文字列を親モジュールの入力属性に与え この文字列の先頭が適したものであるかどうかを結合条件に用いるとトップ・ダウン・パーザが記述できる.また 子モジュールに対応する部分文字列が連続であるかどうかを結合条件とするとボトム・アップ・パーザが得られる.両方式とも自然言語の意味についての属性 属性方程式を導入することによって自然言語処理へと拡張することが可能である.われれはまた Bi-HFPの操作的意味を定義する.Bi-HFPの計算の状態は モジュールの階層的分割関係を示す木(計算木)の集合により表されるが この状態に関する2項関係によりBi-HFPの計算過程は定義される.

著者

片山 卓也

出版者

日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.29, no.4, pp.4_32-4_39, 2012-10-25 (Released:2012-12-25)

---

長年にわたるソフトウェア進化の研究や実務経験にもかかわらず,ソフトウェアを適切に進化させることは容易ではなく,多くのシステムが進化作業の直後に障害を起こしている.この原因がどこにあるかをソフトウェア進化の基本に立ち戻って考え,なぜ進化は困難であるのか,それを克服するための技術課題はなにかを考えた.システムの開発に使われたプロセスの再実行という考えが,進化を考える上で基本的であることに着目し,プロセス主導進化の概念を提案し,これに基づいて進化のあり方や技術チャレンジについて述べた.

著者

片山 卓也 渡辺 治 佐伯 元司 米崎 直樹

出版者

東京工業大学

雑誌

一般研究(A)

巻号頁・発行日

1986

---

属性文法にもとづくソフトウェア自動合成システムの講成法についての研究を行った。このようなシステムの構成には、適切な仕様記述言語とそれで書かれた仕様からソフトウェアを生成するためのシステムが存在しなければならないが、本研究では、それらのいずれをも属性文法にもとづく形式的体系で記述しようとしたものである。元来、属性文法はプログラム言語の意味記述のために導入された形式的体系であるが、その本質は木構造上の関数的計算であり、ソフトウェアやその構成プロセス、ソフトウェアオブジェクトベースの記述には有効な形式的体系である。本研究はこのような観点にたって、ソフトウェア自動合成システムの構成に属性文法にもとづく形式的体系を用いようとしたものである。本研究で得られた主な成果は次の通りである。1.属性文法にもとづく階層的関数型言語AGとそのプログラミング環境SAGEシステムの構成、2.階層的関数型ソフトウェアプロセスモデルHFSPの提案とそのSAGEシステム上での実働化、3.オブジェクト指向属性文法OAGの提案とその評価法、およびソフトウェアデータベース記述への応用。言語AGとその環境SAGEについては、言語の仕様決定、SAGEシステムの各構成要素の設計と構成を行ったが、現在SAGEシステムは一般公開が可能な状態になっている。ソフトウェアプロセスモデルHFSPは、属性文法にもとづく階層的関数型計算モデルをソフトウェアプロセスに適用したものであり、いくつかのソフトウェアプロセスの記述およびそのSAGE上でのプロトタイプ実現を通してその有効性を確かめることが出来た。OAGはオブジェクト指向的機構を用いて属性文法に状態や自己改変概念を導入したものである。OAGの形式化、評価法およびオブジェクトベースの代表的局面の記述を通して、OAGの有効性を確認することができた。

著者

阿草 清滋 落水 浩一郎 片山 卓也 中田 育男 佐伯 元司 鯵坂 恒夫

出版者

名古屋大学

雑誌

重点領域研究

巻号頁・発行日

1997

---

阿草は、既存ソースプログラムを解析しその結果を蓄積するために、細粒度のリポジトリを開発した。CASEツール作成者は、このリポジトリを使うことにより、構文解析や依存解析などのモジュールを作成する手間を省くことができる。ソースプログラムの解析によりライブラリの典型的な利用パターンを発見した。片山は、要求仕様変更とプログラム変更の関係を代数束により形式化し、ソフトウェア発展関係の理論的基礎を与えた。ソフトウェアの段階的詳細化において各段階でプログラムテストを可能とする方式として、抽象実行に基づくソフトウェア構成法を開発した。また、オブジェクト指向開発法の形式化を試み、分析モデルの統合と分析モデルの検証法を与えた。落水は、近年のソフトウェア開発は、分散環境における共同作業であることに注目し、このような環境下でのソフトウェア開発支援のために、開発状況を保持する情報リポジトリを用いて漸進的に情報の矛盾や不確実さの解消を行うモデルを提案し、それに基づく支援環境を構築した。中田は、スライディングウィンドウを持つ計算機の命令レベルの並列化のために、ループのソフトウェアパイプライニングのレジスタ割付方式としてスパイラルグラフを提案した。また、コメントの処理などに必要とされる字句解析器の最短一致法を開発した。佐伯は、再利用プロセスの形式化をユースケースのパターン化とその構造変換規則として行った。分析パターンや設計パターンの構造をパターン化し、必要に応じてホットスポットを埋める手法を提案した。また、ソフトウェアアーキテクチャをカラーペトリネットで形式化し、非機能要求の検証を可能とした。

著者

片山 卓也 島津 明 東条 敏 二木 厚吉 落水 浩一郎

出版者

社団法人人工知能学会

雑誌

人工知能学会誌 (ISSN:09128085)

巻号頁・発行日

vol.23, no.4, pp.529-536, 2008-07-01

被引用文献数

3

著者

片山 卓也

巻号頁・発行日

pp.1-15, 2007-09-07

---

北陸先端科学技術大学院大学 21世紀COEシンポジウム「検証進化可能電子社会」 = JAIST 21st Century COE Symposium “Verifiable and Evolvable e-Society”, 開催:2007年9月6日~7日, 開催場所:キャンパス・イノベーションセンター東京 国際会議室(1F)

著者

泉 直子 片山 卓也

出版者

一般社団法人日本ソフトウェア科学会

雑誌

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

巻号頁・発行日

vol.14, no.5, pp.452-467, 1997-09-16

被引用文献数

1

---

ソフトウェアオブジェクトには製品の部品構成をはじめ,仕様の詳細化関係,バージョン変化など様々な関係がある.オブジェクトを修正する過程でそれらの関係は複雑に変化するので,全体として矛盾なくそれらの関係を保存するのは難しい. 一方,オブジェクト論理はオブジェクトベースを形式的に扱った論理である.オブジェクト論理の一つF-logic[9]は,オブジェクトをis-a関係の階層構造で捉え,オブジェクト間の関係を論理式で与える.更に,オブジェクト識別性,複合オブジェクト,クラス階層,継承などのオブジェクト指向の考え方を保存した解釈を束構造の中に与えている. 本論文では,製品の部品構成,仕様とそこから詳細化してできるオブジェクトとの関係を形式化し,F-logicの拡張として,無矛盾に部品構成の履歴管理ができるオブジェクト論理FT-logicを提案する.更に,形式的な解釈を与え,質問処理に関するアルゴリズムが存在することを示した.