本論文では，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.

We are investigating a way of modeling freight system in the Multiple Ambient Calculus (MAC) and the management systems ensuring the correctness of container handling during shipping using the model. Freight systems have nested structures, i.e., packages (e.g. containers) containing smaller packages (e.g. luggage) that are accommodated by a larger entity such as a container ship. MAC is a formal description language that is suitable for modeling such systems with the 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 containers while, using the Ambient Calculus, 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. The management system propsesed in this paper consists of three sub systems. The first generates formulae that represent freight systems based on several trading documents, the second deploys the formulae to each devices (PCs and RFID tags), the last senses the handling of containers by using UHF RFID devices and checks their consistency with the transitions of corresponding formulae. We also show the results of preliminary experiments in which a car is used as a container.

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.

We present a variant of Ambient Logic to describe desired properties of freight systems and a model checking algorithm for the logic. In the field of distribution, the increase in cargo handling errors is a serious problem as the amount of freight circulation increases. We study a freight inspection system based on Ambient Calculus and we have already built a prototype system. The system can derive process formulas from several freight documents. The system also checks that the actual freight movement conforms the derived formula. To show the correctness of freights transportation, we have to ensure the validity of process formula. We provide an Ambient Logic to present desired properties of freight systems, such as "every cargo will be eventually transported to its destination". We also present an algorithm to show process formula satisfy Ambient Logic formula by exploring state transition graph. We conducted a verification experiment using the model checking system.

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.

In the field of distribution, an increasing of the handling fault of luggage becomes serious problem while the amount of circulation of the freight increases. To solve the problem, we are researching on the constructing the distribution management system based on descriptions of the physical distribution system in the Ambient Calculus. The physical distribution system has the layered structure, e.g., packages (e.g., container) including smaller packages (e.g., luggage) are accommodated by larger entity such as container ships and so on. On the other hand, the Ambient Calculus is a formal description language suitable for representing systems whose layered structure dynamically changes. This feature enables us to express concisely physical distribution systems. The validity of the description can be formally verified with a system of axioms for Ambient Logic. We propose the automatic generating system of the Ambient Calculus formulae, and conformance decision system for the movement of actual freights. The former system generates the formulae that express the transportation route of containers based on the shipping invoice written in Excel files used in an actual container shipping. The latter system checks the movement of an actual freight by comparing it with transition of the formulae. We also present the result of simple experiments to show the effectiveness of those systems.

In this paper, we propose a method to generate test sequences for communication protocols modeled as DFSM with timers. The test sequences can detect any single fault of timer commands or destination states in the transitions on protocol machines. For each single timer command fault, we give sufficient conditions that a given IUT is (or is not) equivalent to its specification. Based on these sufficient conditions, we give a method for generating test sequences. For each destination state fault, we give a test sequence generation method based on Wp-method. To show the usefulness of this method, we developed a system for generating test sequences, and applied it to DHCP (Dynamic Host Configuration Protocol). As a result, we generated the test sequences efficiently.

According to the progress of high-speed networks, many communication protocols are specified as concurrent systems. Such systems can be modeled as concurrent deterministic FSMs (DFSMs). In those protocols, a common input may be taken by some of concurrent DFSMs competitively (non-deterministically). In such a case, the global behavior becomes non-observable non-deterministic in general. In this paper, we propose a conformance testing method based on GWp-method for a sub-class of non-observable non-deterministic FSMs (NFSMs). The proposed method can be used not only for testing NFSMs directly but also for testing concurrent DFSMs whose global behavior is non-observable non-deterministic.

In this paper, we propose a simplification method of structure of distributed computations. In general, distributed computations are modeled as partial ordered events. In order to facilitate analysis of distributed computations, event abstraction has been proposed. Event abstraction reduces apparent complexity of a distributed computation by replacing some related events with one abstract event. The existing method of event abstraction is difficult to use because an analyzer should grasp the structure of the distributed computation. We classified the causal relation of events into two types, that is, the control dependency and the data dependency. Then, we defined the control flow based on the control dependency. In the proposed method, closed control flows are extracted from the distributed computation. Since each closed control flow can be considered as a module in the execution, events involved in a closed control flow are replaced with an abstracted event. To evaluate the proposed method, we implemented a visualization tool of distributed computations based on the method. We applied the tool to some of distributed programs and showed that the proposed method is useful for detecting some kind of programming errors.

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

In 4), a test suite generation method for communication protocols modeled as Finite-State Machine with Counters, a subclass of Extended Finite-State Machine (EFSM), is proposed. In this paper, a practical evaluation of fault detection power of test suites generated by the method and several other test generation methods. For the evaluation, we developed a mutation system which derives implementations with single or double faults from correct protocol implementation in C program. We examined whether the test suites can detect faults in the derived mutations. The experiment has shown that the fault coverage of the method proposed in 4) is superior to other methods.

In this paper, we propose a condition of test cases for communication protocols modeled as FSM with counters(FSM-C), a subclass of Extended Finite-State Machines(EFSM). By using test cases satisfing the proposing condition, single fault of on determinig inequality or register assignments can be detected. We also propose a procedure to find test cases which satisfy the condition. To see the usefulness of this method, we developed a test cases generating system based on the proposing method, and applied the system to the OSI session protocol. As a result we can verify that all of test cases are generated automatically.

本論文では不変式を用いた拡張有限状態機械モデルの通信プロトコルの検証における不変式記述作業の軽減を目的に, 積和形で記述される不変式の積項の大部分を機械的に生成する手法について述べる. 提案手法では, 一方のプロトコル機械のメッセージの送信に同期して他方のプロトコル機械のメッセージの受信が行われる同期型通信で到達可能な状態とそれらの状態からメッセージの送信のみによって到達可能な状態で成り立つ積項の生成を行う. 本手法に基づく不変式の半自動生成システムを試作し, 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の故障診断法を提案し、その故障検出能力をシミュレーションにより評価した。

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

We investigated the Multiple Ambient Calculus(MAC) and Hybrid Timed Ambient Calculus(HTAC) for specifying freight systems. We proposed a condition for HTAC formulae considered as freight specifications. We also proposed a model checking algorithm based on a congruence relation of HTAC formulae. For constructing freight management systems, we constructed a distributed freight management system based on MAC using UHF RFID devices and conducted a preliminary experiments.

We investigate extensions of the Ambient Calculus for specifying freight systems, which include various timing constraints and deal more than thousands of container objects. For specifying timing constraints, we propose the Timed Ambient Calculus by introducing capabilities with expiration time, waiting capability, and special ambient to express timing violation. For dealing with large amounts of container, we propose the Multiple Ambient Calculus, which enables us to model freight systems by a set of formulas. We also investigate model checking on the extended calculus and the way for constructing distribution monitoring systems based on the formulas in the extended calculus.

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

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