本論文では，Ambient Calculus（AC）を時間的な制約が記述できるよう拡張した混合型時間アンビアント計算（HTAC）と，それを用いた物流計画記述法を提案する．HTACはACのケーパビリティに加えて，有効期限付きケーパビリティと待機ケーパビリティを持つ．これにより，ACの特徴であった階層構造の動的な変化の表現に加え，タイムアウト動作や2つのイベント間の発生間隔の上下限の指定などの時間制約が指定可能となる．有効期限付きケーパビリティを連続するイベントが離散的に発生するオブジェクトの移動の表現に用い，ACのケーパビリティを瞬時に発生するべきオブジェクトの移動情報の通知などに用いることで，各種交通機関を用いた人の移動や海上物流などの物流計画が記述できる．このようなケーパビリティを使い分ける基準として，プロセス式が物流計画の記述と見なせるための条件を与える．また，HTACプロセス式から実行可能なイベントを選択し，式を遷移させる処理系を開発した．この処理系を用いて，プロセス式が意図どおりの動作をするかなどの確認を行うことができる．その処理系を活用した物流監視システムの構築方法について述べる．物流監視システムはHTAC式による物流計画に違反したオブジェクトの移動を検出するとともに，HTAC式に沿った移動を誘導するようなシステムである．In this paper, we propose the hybrid timed ambient calculus (HTAC) as an extension of the ambient calculus (AC). We also propose a way for specifying logistics plans using HTAC. In addition to the capabilities of AC, HTAC contains expiration time and waiting capabilities that enable us to specify timeout-like behaviors and specify the lower or upper bounds of the timing interval between two events. Therefore, we can represent logistics specifications such as human travel plans with various transportation systems or maritime logistics. In HTAC logistics specifications, we use the expiration time capabilities for physical movements, which occur discretely, and the original AC capabilities for the physical movement notifications, which occur simultaneously. We give a condition for the HTAC formula, which is regarded as a logistics specification. We developed a formula processing system, which can reduce a process formula by selecting executable events, enabling us to confirm whether the process formula behaves as intended. We will describe the method to build a logistics monitoring system with the formula processing system. The system can detect the physical movement that violates the logistics plan, or can guide the movements in compliance with the logistics plan.

We propose an integrated development environment (IDE) for developing formulae written in the multiple ambient calculus (MAC). MAC is a kind of process algebra designed for modeling freight systems in which a lot of containers are transported by several vessels from one port to another port via several hub ports. We have been studying a handling management system that confirms the validity of container handling during shipping. The system checks whether containers are being correctly handled by comparing the movement of the containers, which is sensed by radio frequency identification (RFID) tags, with formal models (formulae) written in MAC. For accurate and automatic management, we need to develop MAC formulae that accurately express the nested structure of the entire freight system (ports, vessels, and containers) and the movement of those objects. The IDE presented in this paper (IDE4MAC) enables us to develop such formulae with ordinal editing functions and several debugging functions such as a selective execution function and backward tracing function that are useful for checking all non-deterministic actions of MAC processes. We developed IDE4MAC as plugins of Eclipse so that it can be easily installed and used.

We are developing a freight management system that confirms the correctness of container handling during shipping. The system determines the correctness by comparing container handling, which is sensed by UHF RFID tags, with formal models (formulae) written in the Multiple Ambient Calculus(MAC). MAC is a formal description language extended from the Ambient Calculus(AC) in order to express freight systems with nested structures that dynamically change. Using MAC, whole the freight system is modeled by a set of formulae each of which represents the handling of each container while, using AC, the freight systems are modeled by a large formula. Thanks to this feature of MAC, we can express symmetric and concurrent property of freight systems more appropriately and adding or retracting formulae (representing adding or canceling containers for a voyage) becomes easier than using AC. This paper shows the implementation of the freight management system and the results of several experiments.

We propose an integrated development environment (IDE) for developing mobile processes written in the ambient calculus (AC). AC is a kind of process algebra designed for modeling mobile processes in network environments. This IDE is equipped with not only ordinal editing functions but also characteristic ones for AC: a graphical editor for describing tree structures of AC processes that can be converted to AC processes, a selective executing function and backward tracing function that enable us to check every non-deterministic action of AC processes, a distributed executing function for mobile processes that enables us to debug those processes in a network environment by deploying IDEs, and the ability for Java programs to be conveyed by ambients while keeping their activated conditions. We developed the IDE as plugins of Eclipse.

我々は,多重Ambient Calculus(MAC)による物流システムの記述方法の研究および,実際の物流が正しく行われているかを監視するシステムの開発を行っている.物流システムは,より小さなパッケージをより大きなパッケージに収容する階層構造を持っている.これに対し,プロセス代数の一種であるMACは,階層構造を持ち動的に構造が変化するシステムを形式的に記述できる.MACは,通常のAmbient Calculus(AC)と異なり,個々の貨物の取扱いを個別のプロセス式として記述し,それらの集合により物流システム全体をモデル化するものである.この特徴により,通常のACと比較して物流システムの持つ対称性,並行性をより適切に表現でき,貨物が追加,削除される際のプロセス式の変更も容易となる.本稿では,MACとUHF帯RFID機器を用いた物流監視システムを提案する.本システムは,実際のコンテナ輸送で使われる数種類の書類をもとに,各コンテナの搬送経路を表現するMAC式を自動生成するシステム,MACの個別式を適切な端末へと分散するシステム,およびRFIDを用いて検知した貨物の動きや,船の乗り換えがMAC式の遷移に沿ったものであるかを監視するシステムからなる.また,本システムの有用性を示すために,車をコンテナと見立てて行った屋外実験についても述べる.

This paper proposes a freight management system that confirms the correctness of container handling during shipping. The system determines the correctness by comparing container handling, which is sensed by UHF RFID tags, with formal models (formulae) written in the ambient calculus. The ambient calculus is a formal description language that is suitable for expressing freight systems with nested structures that dynamically change. The management system generates formulae automatically from several documents used in real freight systems. An implementation of the system and the results of several experiments using it are presented. © 2012 IEEE.

本論文では物流システムの満たすべき性質の形式的な記述体系とそのモデル検査について述べる.物流の世界では,貨物の流通量の増加にともないコンテナ管理の重要性が高まっている.我々はAmbient Calculusによる物流システムの記述と,実際の物流がその記述どおりに行われているかを監視するシステムを開発した.この監視システムによる物流管理の正しさを確認するためには,書類から生成されたプロセス式そのものの正当性を確認する必要がある.しかし,プロセス式生成システムで生成されるプロセス式は一般に複雑なものになり,さらに非決定的な動作も多くこの確認作業を人手で行うのは困難であると考えられる.本論文では,この課題を解決するために,物流システムに要求される,"いつか必ず貨物は目的地に輸送される" というような性質をAmbient Logicの論理式で表現し,その性質をプロセス式がすべて満たしていることを形式的に検査する手法を提案する.また,提案手法に基づくモデル検査システムを構築し検証実験を行った結果についても述べる.

We investigate a management system that ensures the correctness of cargo distribution in freight systems The system determines the correctness by comparing the movement of containers, which sensed by IC tags with formal models. These models are written in the ambient calculus and generated automatically based on several documents used in real freight systems. The ambient calculus is a formal description language that is suitable for representing freight systems with nested structures that dynamically change. An implementation of the system and the results of a simple experiment using it are presented.

物流の世界では,貨物の流通量が増加する一方,コンテナ管理の重要性が高まっている.我々はその解決策としてAmbient Calculusによる物流システムの形式的記述に基づく物流管理システムの構築について研究を進めている.物流システムは,荷物,コンテナ,コンテナ船というように,複数のより小さなパッケージを収容したパッケージがより大きなパッケージに収容されるという階層構造を持っている.一方Ambient Calculusは,階層構造を持ち動的に構造が変化するシステムを形式的に記述するための言語であり,この特徴から物流システムの持つ階層構造を簡潔に表現することができる.さらにAmbient Logicの公理系を用いて記述の正当性を形式的に検証することが可能である.本論文では,実際のコンテナ輸送で使われるExcel形式の送り状をもとに各コンテナの搬送経路を表現するAmbient Calculus式を自動生成するシステム,Ambient Calculus式をもとに実際の貨物の動きが式の遷移と適合しているかどうかを検査するシステムについて述べる.また,オンボードLinuxを装備した箱をコンテナに見立ててこれらのシステムの有効性を調べる実験を行った.その結果についても報告する.

本論文では, オペレーティングシステムのタイマ機能を利用するDFSMモデル通信プロトコルに対して, 状態遷移におけるタイマ操作の単一誤りおよび終状態の単一誤りを検出する適合性試験系列生成手法を提案する.タイマ操作誤りについては, 個々の誤りに対してプロトコルの仕様と実装が等価になるための十分条件と等価にならないための十分条件を与え, これらの条件を利用した試験系列生成手法を考えた.終状態誤りについては, Wb法を利用した試験系列生成手法を考えた.提案手法の有効性を確認するため, 提案手法に基づく試験系列生成システムを実装し, DHCP(Dynamic Host Configuration Protocol)に適用した.その結果, 試験系列が効率的に生成できることを確認した.

高速ネットワークの発展にともない, 多くの通信プロトコルが提案されている.そのようなプロトコルのいくつかは, 複数個の決定性FSM(DFSM)群が協調して動作し, それらのDFSM群が共通の入力を奪い合って非決定的に動作するようにモデル化できる.そのようなモデルでは, システム全体の動作として, 観測不可能な非決定的動作を含む場合がある.本論文では, そのような観測不可能な非決定的動作を含む並行DFSM群に対して, GWp-法に基づく1つの適合性試験手法を提案する.

本論文では分散計算の解析を容易にすることを目的とし, 各プロセスにおける制御フローに着目して分散計算の構造を簡略化する手法について述べる.分散計算は, 一般にそれぞれのプロセスで発生するイベントの半順序集合として表すことができる.大規模な分散計算の解析を容易にすることを目的として, 複数のイベントを1つの抽象イベントに置き換えることによって計算全体の構造を簡単化するイベントアブストラクションという手法が提案されている.従来提案されている手法では, 解析者が計算全体の構造を把握する必要があるため, 解析者の負荷が大きいという問題がある.提案手法では, イベント間の因果関係を制御依存関係とデータ依存関係に分類し, 制御依存関係に基づき計算中の閉じた制御フローを抽出する.1つの閉じた制御フローは分散計算中のひとまとまりの処理と考え, これを1つの抽象イベントに置き換えることにより計算全体の構造を簡略化する.提案手法の有効性を議論するため, 実際にイベントアブストラクションを行い, 結果を可視化するツールを作成した.そして, いくつかの分散プログラムの実行結果に作成したツールを適用し, バグの検出に一定の有効性があることを確認した.

属性ベースによるファイルシステムのための名前管理方式として、 階層的に管理されたキーワードをファイルに付与する方式を提案しプロトタイプシステムを実装した。

本稿では拡張有限状態機械(EFSM)モデルの通信プロトコルに対する適合性試験系列の現実的な誤り検出能力の実験的評価について述べる.評価実験に際して,プロトコル仕様を正しく実装したCプログラムからC言語上のフォールトを1個または2個含む実装を生成し,その実装が試験系列を正しく実行するかを観察するシステムを開発した.2つの例プロトコルを対象に,これまでに提案された各種試験系列生成手法による試験系列の誤り検出能力を評価した結果,文献4)の手法は他の手法より誤り検出能力が高いことが確認できた.

本論文では, 拡張有限状態機械(EFSM)のサブクラスであるカウンタ付き有限状態機械(FSM-C)としてモデル化された通信プロトコルに対して, そのレジスタ操作の正しさを試験する系列が満たすべき条件, およびそのような系列が存在するときそれを生成する手順を提案する.本手法を用いて生成した試験系列を用いると, 遷移条件の条件判定およびレジスタ代入操作の単一誤りを検出できる.また, この手法の有効性を確認するため, 提案手法に基づく試験系列生成システムを作成し, OSIセションプロトコルに対して実験に試験系列の生成を行った.その結果, すべての試験対象に対して試験系列が存在し, 自動生成できることが確認できた.

本論文では不変式を用いた拡張有限状態機械モデルの通信プロトコルの検証における不変式記述作業の軽減を目的に, 積和形で記述される不変式の積項の大部分を機械的に生成する手法について述べる. 提案手法では, 一方のプロトコル機械のメッセージの送信に同期して他方のプロトコル機械のメッセージの受信が行われる同期型通信で到達可能な状態とそれらの状態からメッセージの送信のみによって到達可能な状態で成り立つ積項の生成を行う. 本手法に基づく不変式の半自動生成システムを試作し, OSIセションプロトコルのデータ転送フェーズから抽出した例プロトコルの検証実験に適用したところ, 不変式をほぼ自動的に生成することができた.

複数のサブプロトコルの組合せによって大規模プロトコルを定義する手法の一つとして,Chowらはフェーズと呼ばれる一定の性質を満たすプロトコルを直列連結する手法を提案している.但し,彼らの連結法では連結のための条件として,プロトコル機械が有限状態機械としてモデル化されること,フェーズ終了時に双方向の通信路がともに空になっていることを仮定している.本論文では,それら二つの制限を緩和した,より一般的なフェーズ連結手法を提案する.本論文で提案する手法を用いることにより,例えばトークンパッシングを行うプロトコルを,トークンが一方のプロトコル機械に固定されている二つのフェーズの連結によって定義することが可能となる.

プロトコル機械が拡張有限状態機械でモデル化され,通信路が非有界FIFOでモデル化された通信プロトコルの生存性の検証法を提案する.生存性は初期状態から到達可能な任意の状態から興味のある性質Qを満たす状態に到達可能であるという性質(Q-live性)として定式化する.性質Qはプロトコル機械の状態および通信路上のメッセージ系列に関する条件を表す4種類の原子論理式を用いて指定する.それらの原子論理式を用いて,人間の検証者が初期状態から到達可能な状態の集合を部分集合RS_1,RS_2,...,RS_nに分割する.このとき,各頂点v_i(1≦i≦n)がRS_iに対応し,「∀gs∈RS_i∃gs′∈RS_j{gsからgs′に到達可能である}」ときに限りv_iからv_jへの辺があるようなグラフを縮退到達可能性グラフと呼ぶ.本論文では,与えられたRS_1,RS_2,...,RS_nに対して縮退到達可能性グラフを構成し,それを探索することによるQ-live性の検証法を提案する.また,提案する検証法に基づいて試作した検証システム,およびOSIセションプロトコルの一部を抽出したプロトコルのQ-live性の検証を行った結果についても述べる.

本書は、プログラムを作った経験の無い人や計算機を操作することにようやく慣れてきたくらいの学生を対象に、今日ソフトウェア産業の中で主流となっているオブジェクト指向プログラミングを、Java言語を用いて学んでいきます。

本書はUNIX・Linux に関する実用的な入門書である。対象は大学理工系学部の学生だが、他学部や高専の学生にも利用できるように、全体を基礎部分と応用部分とに大別している。基礎部分では、UNIXを学習するすべての学生に必要な事項であるファイルシステム、コマンド、シェル、ウィンドウ、エディタ、メール、シェルスクリプトについて解説している。応用部分では、文書作成(LaTex)、ホームページ作成(HTML)、プログラミング言語(C及びFORTRAN)、数理解析(Mathematica)、GUIプログラミング(Tcl/Tk)のような独立した章を用意しており、必要な章だけを選んで学習できるように構成している。

動的に変化する階層構造を持つシステムの記述向けのプロセス代数であるAmbient Calculus を時間的な制約が記述できるよう拡張した時間付きAmbient Calculus を提案した． これにより、タイムアウト動作や，2 つのイベントの発生間隔の下限と上限の記述が可能となった．

本稿ではp プロセッサを用いたHBSP モデル上で、サイズn × n の2 次元データに対し、各プロセッサの速度に応じてデータを割り当てるデータ分割法を示し、また、その分割法を用いた行列積を解く並列アルゴリズムを示す。

時間に依存した動作を行う通信システムをモデル化したタイマ付きFSMの故障診断法を提案し、その故障検出能力をシミュレーションにより評価した。

属性ベースのファイル名管理方式の一つとして、階層的に管理されたキーワードをファイルに複数個付与する方式を提案し、実装上の問題点を議論した。

物流計画の記述に適用するためのAmbient Calculusの拡張として多重アンビアント計算(MAC)、混合型時間アンビアント計算(HTAC)を策定し、その応用として物流計画の記述スタイルの検討、モデル検査手法、物流監視システムの構築法について検討した。 記述スタイルについてはHTACを対象にプロセス式が物流計画として妥当とみなせる条件を提示した。モデル検査手法についてはHTACを対象として、合同的性質を活用した検査の効率化手法を検討した。物流監視システムの構築についてはMACによる物流記述を対象にUHF帯RFID機器を利用した監視システムの構築および模擬的な監視実験により実現性を確認した。

昨年度に引き続いて、物流管理システムの構築への応用を想定し、動的に変化するオブジェクトの階層構造の記述に適したプロセス代数であるAmbient Calculusの拡張に関する研究を進めた。昨年度定めた時間付きAmbient Calculusの構文規則、遷移規則に基づく直接実行系の実装を進めた。一方Ambient Calculusないしは時間付きAmbient Calculusで実際の海上物流などの物流システムを記述しようとする場合、取り扱う貨物の数が膨大なものとなるためプロセス式が複雑なものとなってしまう。物流システム記述の正当性確認のためのモデル検査、あるいは記述に基づく物流管理システムの構築を考えると、なるべく単純な構造のプロセス式により物流システムの持つ対称性、並行性を適切に表現することが重要になる。そこで本研究では、単純な構造での大規模プロセス式の記述を可能とするため、Ambient Calculusの拡張として、複数のプロセス式の組で物流システムを表現する多重Ambient Calculusを提案した。さらに多重Ambient Calculusのプロセス式間の等価関係として弱双模倣関係に着目し、この関係がプロセス式の追加操作について閉じているなどのいくつかの性質を示した。さらに弱双模倣等価性を活用して、多数の貨物を扱う物流システムの正当性確認のためのモデル検査を、より少数の貨物のモデル検査と、それらの間の弱双模倣等価関係の確認に帰着する方法を考案した。さらに考案した方法に基づくモデル検査システムを実装し、検証実験によりその有効性を確認した。

分散データベースにおける逐次化グラフを用いた分散制御によるスケジューリング手法に関し,従来提案していたアルゴリズムを基に以下の研究を行なった. (1)提案アルゴリズムのシミュレーション評価:提案アルゴリズムを種々の環境で用いた場合の有効性を評価するため,種々の条件下でシミュレーションを行ない,トランザクション実行時のスケジューリングのために必要となるメッセージの通信量などを算出した.その結果,提案アルゴリズムは他のアルゴリズムと比べてデータアクセスの局所性の影響を受けやすいほか,分散型データベースを構成するサイト数が多いときにより有効であるということがわかった. (2)障害回復可能なアルゴリズムの提案:従来提案していたアルゴリズムは,(i)逐次化グラフ検査に時間がかかる,(ii)サイト障害などの故障から回復できない場合が存在する,という問題点がある.この問題を回避しうるスケジューリングアルゴリズムとして,(i)すべての操作をただちに実行しトランザクション終了時にその有効性を検査する,(ii)局所的コピーを用いて実際のデータベースへの書き込み操作を遅らせることにより障害からの回復を可能にする,ことを特徴とするアルゴリズムを提案し,その正当性の証明,シミュレーションによる基本性能の評価を通じて有効性を示した.

拡張有限状態機械でモデル化される通信プロトコルの安全性検証のための,不変式の記述支援に関し以下の研究を行なった.(1)不変式の一部の自動導出手法の検討:二つのプロトコル機械の送信したメッセージのすれ違いがないという条件のもとで到達可能な状態に関する積項を順次生成する手続きを与えた.与えた手続きでは,一部人間の検証者との対話的処理を行なう.(2)不変式の半自動生成システムの試作:前記手法の実現性を確認するため,報告者らが既に開発していた拡張有限状態機械モデルの通信プロトコルの検証システムの一部として,不変式の半自動生成システムを試作した.実現のために記述したプログラムは約6,000行であった.(3)例プロトコルの検証実験:OSIセションプロトコルのデータ転送フェーズから抽出した例プロトコル(各プロトコル機械の状態数:10,整数値レジスタ数:2)の検証実験を行なった.上記の不変式半自動生成システムは例プロトコルに対し,632個の積項を出力した.それらの積項の和をとることにより得られた論理式が,例プロトコルの不変式であること及び安全でない状態では成立しないことが検証システムにより示された.以上より,例プロトコルの安全性がほぼ自動的に証明された.