Search

In this paper, we propose an application layer multicast protocol called Emma/QoS. Emma/QoS manages multiple multicast video steaming flows in a fully distributed manner so that the user gain in receiving those flows can be maximized. Emma/QoS assumes that each end-host is capable of filtering streaming flows when relaying them to the other end-hosts. Using this functionality, Emma/QoS (a) accommodates a request of a new video source by degrading the bit-rates of the existing video streams, and (b) adjusts their transmission rates according to given user benefit functions, which can be application-specific. Simulation results have shown the efficiency of Emma/QoS.

A variety of studies on face components such as eyes, lips, noses, and teeth have been proceeding in medicine, psychology, biometrics authentication, and other areas. In this paper, we present an algorithm of extracting eye contours from a face image using the deformable template matching method. Our template for an eye contour is composed of three quadratic functions for the perimeter and one circle for the pupil. In our algorithm, a digital color face image is rst converted to a binary image of representing eyes, after the region around eyes is identied on the face image by using hues and values of the color image. Then, parameters in the template are optimized by a local search method with a tabu period and a hill-climbing, so as to t the template to the eye contour in the binary image. The accuracy of our algorithm is evaluated through sample face images of students. In addition, the application of our proposal to eye shape indices is investigated in a face image database "HOIP", where recognizable dierence exists in index distributions between males and females.

整数変数をもつ有限状態機械（FSM/int）に対する記号モデル検査法を提案する．入力値を保持する変数の値は次に同一遷移で新たな値が読み込まれるまで変更されない，などの制約を満たす，与えられたFSM/intに対し，整数変数をもつCTL式を満たすか否かをこの記号検査アルゴリズムは判定する．この記号モデル検査アルゴリズムを実装し，ブラックジャックディーラ回路とパケット多重化プロトコルに適用した．そして，100状態，10整数変数程度の規模のシステムであれば数秒程度（最悪時で数分程度）で検証できることが確かめられた．

計算機を用いてソフトウェアプロセスの実行を支援する場合，技術者の作業内容とそれらの実行順序に加え，技術者間のデータ交換などの連絡作業の内容とそれらの実行順序を定める必要がある.しかし，これらの連絡作業を陽に記述するのは繁雑で誤りも多いため，我々は，レジスタ付ペトリネットモデルを用いてプロセス全体の要求仕様を連絡作業なしで記述し，その記述から各技術者における連絡作業を含む動作仕様を自動生成する方法を考案している.本稿では，考案した手法に基づき，技術者の動作仕様群を自動生成するシステムと，それらの動作仕様群を分散実行してプロセスの実行支援を行うシステム(実行支援系)の設計の概略について述べる.設計した実行支援系の実働化により，技術者の負担が軽減され，作業効率が上がることが期待できる.また，現実のソフトウェア開発を考慮した機能設計を行うことで，より実用的な開発支援を実現することを目指す., In order to enact a software process in a distributed environment，it is necessary to specify the engineers' work，communications between the engineers，and their temporal orders in the process. However，since it is so complicated to describe the communications，the designers may make mistakes in the process description. We have proposed a method to derive correct engineers' individual descriptions with communications from the whole description of a software process without communications，using a Petri net model with registers. In this paper，we have developed a derivation system according to the proposed method，and designed a support system which executes the derived individual descriptions in a distributed environment in parallel. It is expected that the efficiency of the engineers' work is improved since the engineers' burden becomes light using these systems. The goal of this study is to provide more practical support facilities for the software development.

本論文では，加算をもつ有理数の理論（有理数変数，有理数定数，+,-,=,n^＜γ d (b+1)＾a >（α,β,γ は定数，n は入力の式に含まれる不等式の個数，d は変数の個数，a は限定子交替数，b は同じ限定子が続く最大の個数，r は入力の式の各係数と定数の分母，分子のビット数）の計算幾何学の手法を利用した真偽判定アルゴリズムを提案する．従来知られていた真偽判定アルゴリズムの最良の時間計算量は r ・ 5^n^（ε,ζ は定数）である．

動作の実行時刻に制約のある分散システムのサービス仕様（システム全体が1計算機で実行されるとしたときのその計算機の仕様）から計算機間の通信遅延を考慮してもその制約を満足するプロトコル仕様（実際の計算機ごとの仕様の組）を自動合成する手法を提案する．提案手法では，多くのリアルタイムシステムの仕様記述，検証に用いられている時間ペトリネットに基づくモデルを用い，従来手法において必要とされていた計算機間での同期時計を必要としないプロトコル仕様を合成できる．また，状態変数を含むサービス仕様からの合成もできる．サービス仕要を満足するプロトコル仕様が存在するかどうかを判定することや，存在する場合にある評価基準のもとで最適なプロトコル仕様であるかどうかを保証することは容易ではないが，本手法ではそれらの問題を線形計画問題に帰着し，それらを機械的に判定，求解する工夫をしている．本手法を用いることで，計算機間の通信遅延を直接計算することなく仕様記述が行えると考えられる., In this paper, we propose a method for deriving a protocol specification of a real-time distributed system from a given service specification with time constraints. In our method, a protocol specification can be derived without synchronous clocks among protocol entities, using a time Petri net based model. In addition, a service specification with state variables can be also treated.In general, it is not easy to check whether protocol specifications satisfying the required services exist or not, and to get the optimal one if they exist. We formulate it to linear programming problems and get the optimal protocol specification. Using our method, designers do not need to consider communication delays amon protocol entities directly, on specifying real-time distributed systems.

本論文では，各状態からの遷移条件がその状態の訪問回数で決まる有限状態機械モデルの上で生存性の検証を機械的に行う1つの方法を提案する．通信プロトコルは有限状態機械（FSM）によってモデル化され検証される場合が多いが，一般にシーケンス番号などのパラメータ値の変化を直接状態で区別して表そうとするとFSMの状態数が多くなり，状態爆発が起こる．我々は各遷移の実行可能性がその遷移の開始状態の訪問回数で決まるような有限状態機械モデルFSM／Cを提案し，このFSM／Cモデルの上で整数線形計画法を用いることにより状態爆発を回避した生存性の検証法を提案する．FSM／Cモデルでいくつかの通信プロトコルの仕様を記述できる．また，この手法に基づき，FSM／Cからなる通信系の生存性を検証するシステムを作成した結果についても報告する., Many communication protocols are modeled as finite state machines(FSM's).In general,since the size of states becomes large in order to treat parameter values such as sequence numbers,the state explosion problem may occur.In this paper,we will propose an FSM/C model where the execution of each transition may depend on the number that its starting state has been visited,and propose a technique for verifying a liveness property.In this model,a counter Csi holds the number that state si has been visited.Many communication protocols can be modeled in our FSM/C model.If two communicating FSM/C's eventually return to the pair of their initial states and the communication channels become empty,thenwe say that they have the liveness property.For verifying the liveness property,we use an integer linear programming technique so that the state explosion problem does not occur.

本論文では，共有メモリをもつマルチプロセッサ上での正則な項書換え系の効率の良い一実装法を提案する．提案する方法では，(1)「eventually outermost書換え系列」に基づく書換え方法をとっていること，(2)有限状態機械をマッチングの際に用い，そこで得られた情報を次回以降のマッチングの際にマルチプロセッサ環境上で再利用していること，(3)多くの研究が特定のアーキテクチャに依存しているのに対し，特定のアーキテクチャに依存せず並列性を本質的に利用していること，等の特徴をもつ．提案する手法を評価するために並列項書換え過程を模倣するシミュレータを作成した．このシミュレータを用い，処理時間，CPU利用率の計測を行った．与えられた項が十分大きいときには提案する方法で効率良く書換えが実行されることが確かめられた．

近年の大規模なグラフィカルユーザインターフェース (U) プログラムにおいて，GUIの制御部はより複雑になる傾向にある．そのような制御部の設計法のひとつとして，まず，各GUI部品 （オブジェクト） とイベントの表 （オブジェクト属性表），さらに，内部処理の集合を決定し，GUIの動作を記述したシナリオ群からタイムオートマトンで記述されたGUIの全体動作記述を自動導出する．そして，その全体動作記述から時間制約処理部と各オブジェクトの動作仕様群を自動導出するという方法を提案する．本手法の利点は，(） シナリオが優先度を持つこと，(） 時間制約を記述できること，(） 全体仕様と各オブジェクトごとの動作仕様の二つを導出することにより，全体動作の把握と，GUIに特有なオブジェクト指向プログラムによる実装が容易になることである., Recently, controllers of Graphical User Interface (GUI) programs become rather complex. We propose one method for designing such GUI controllers. In our method, first, a whole specification (abstract level specification) of a GUI's controller is derived automatically as a timed automaton from scenarios which describe the GUI's partial behavior, using a relation table of events and objects (corresponding to widgets such as buttons, scroll bar and so on) and a name list of primitive functions used in the program. The timed automaton is automatically divided into a set of concurrent timed automata (lower level specification), each of which describes behavior of the GUI's object. Advantages of our method are the following. (a) Each scenario has a priority. The priority is used to derive a rather complex whole specification from simple scenarios. (b) Timing restrictions such as time-out and wait and so on, can be described. (c) The method derives two levels of specifications. The abstract level specification helps us to understand the whole behavior of the GUI program. The lower level specification helps us to implement the program in the object oriented programming style.

プロトコル合成法は分散協調システムの設計において，通信動作の記述の誤りをなくし，設計者の負担を軽減する有用な手法の一つであり，これまでにさまざまな計算モデルを用いた手法が提案されている．しかし，システムの状態変数を扱うことができ，かつ並列動作や選択動作などを含む制御構造が記述できるクラスに対する合成法は提案されていない．本論文ではレジスタ付きペトリネットモデルに対する一つのプロトコル合成法を提案する．提案する手法では，p個のノード（計算機）とそれらの間の信頼できる通信路からなる分散システムを対象とし，そのシステムの全体動作仕様と，各ノードへのゲートやレジスタの配置指定が与えられたときに，全体動作仕様どおりの動作を行う各ノードの動作仕様の組（分散動作仕様）を自動合成する．また，提案した手法に基づく合成系や実行系を試作し，協調活動の支援に適用することにより本手法の有用性を示す．

条件付き項書換え系は, 条件付き書換え規則における, 規則左辺に出現しない変数 (extra variable, 照合外変数と訳した) の分布の状況によって, いくつかのクラスに分類される. 本論文では,「規則右辺の変数は, 規則左辺に出現する変数か, 条件に出現する照合外変数でなければならない」というクラス (3-CTRSs) に対し, 階層合流性 (level-confluence) を満たすCTRSの直和 (disjoint union) は階層合流性を満たすことを示す., It has been proved that every disjoint union of level-confluent conditional term rewriting systems (CTRSs) with extra variables in the conditions of the rewrite rules is also level-confluent. In this paper, we show that this statement is also valid for CTRSs with extra variables in the right-hand sides of the rewrite rules.

リアルタイム分散システムを設針する一つの手法として,各動作の生起時刻に時間制動が与えられた分散システムの全体仕様から,ノード(計算機)間の通信路の遅延時間等を考慮して,与えられた時間制約を満たしながらメッセージ交換を行い,全体仕様通りの動作をする各ノードの動作記述を自動導出する手法が提案されてきている.しかし,従来の手法では,並列動作の同期や,システムのリソースを取り扱えないクラスに制限されていた.本稿では,並列動作やその同期,非決定的選択動作が記述でき,かつリソースを扱えるレジスタ付き時間ペトリネットモデル(TPNRモデル)を新たに提案し,そのモデルで記述された分散システムの全体仕様と各ノードへのリソースの配置指定,ノード間の通信路の最大遅延時間,ノード間のクロックの最大誤差が与えられたときに,(1)全体仕様で与えられるシステムが分散システムとして実行可能であるか(分散実行可能性)を判定し,(2)可龍である場合には全体仕様の時間制約を満たす各ノードの動作記述を自動導出する手法を提案する.提案する手法では,メッセージ交換の仕方などに一定の方針(模倣方針)を定め,その模倣方針のもとでの分散実行可能性判定を線形計画問題に帰着し,各ノードの動作を実行可能な時刻の幅の総和を最大にする解を得ることで,動作の実行時刻に関して自由度の高い動作記述を得る工夫を行っている.本手法により,設計者自身が通信動作に要する遅延時間を詳細に検討せずに,動作の実行可能時間幅の広い動作記述を自動生成できる,通信動作を直接記述する場合の誤りをなくすことができる,などの効果が期待できる., Some methods for deriving protocol specifications of real-time distributed systems from given service specifications with time constraints (deadlines of actions) have been proposed. However, these methods cannot treat the class of service specifications including parallel synchronization and parameters. In this paper, we propose a method for deriving a protocol specification automatically from a given service specification in an extended model of time Petri nets, called a Time Petri Net model with Registers (TPNR model). In our derivation algorithm, a resource allocation specifying the allocation of resources to the protocol entities, each maximum communication delay between two protocol entities, and a maximum error among the clocks of the protocol entities can be specified freely by the designers. The algorithm (1) decides whether the service specification can be implemented in the protocol entities satisfying the deadlines of actions using a method for solving linear programming problems, and if so, (2)derives a protocol specification, where the sum of the ranges of all deadlines can be maximized. Using our method, the designers will be free from considering the details of communication delays on the design of real-time distributed systems.

代数的手法を用いた階層的設計法として，我々は要求仕様から実現プログラムまで同一の詳細化法に基づいて段階的に順次詳細化する方法を提案している．各レベルでは，そのレベルでの関数，処理の性質等の要求記述が行われ，そのレベルで閉じた記述になっている．上記の方法で順序機械型記述を行う際に，（イ）興味ある関数に対する要求のみ取り出す拡張射影を用いる方法，および，（ロ）通常のように前提条件を内部データに関する具体的な述語を用いて記述せず，外部入力の条件と実行制御上の条件で定義される到達正当性条件を用いて記述する方法等が有用であることが既にわかっている．本論文では，拡張射影あるいは，到達正当性条件を用いて記述された順序機械型記述間において，正しい詳細化であることを形式的に定義し，そうであることを示すための証明方法について新たに述べる．詳細化の自由度を大きな範囲で許しているにもかかわらず，これらの証明方法は従来の記述法に対する証明方法で必要とする手間や，考案すべき言明の量と比べ遜色がない．

グループワークの支援システムを複数の計算機による協調計算システムとしてみなすことができる。そこで、グループワークの各作業をゲートに対するデータの入出力と（ファイル等を表す）レジスタの更新式として抽象的にとらえ、グループワーク全体の作業順を拡張有限状態機械モデルとしてモデル化する。また、その記述（全体動作仕様）と、各計算機へのゲートとレジスタの配置指定等から、グループワークを支援する各計算機の作業手順（該当する作業者の作業手順やデータの入出力のほか、他の計算機とのデータの交換などの通信動作も記述されたプログラム）を自動生成するアルゴリズムを、従来のアルゴリズムを拡張することによって考案した。また、この導出アルゴリズムの処理系（生成系）を作成し、導出時間の評価を行った。また、導出した動作プログラム群を並列に実行する分散実行系を作成し、実行時間等の評価を行った。本アルゴリズムは、全体動作仕様と配置指定等を区別することにより、作業者へのグループワーク内の作業の割当ての変更に柔軟に対応できる等の利点がある。また、各処理系の実験評価から本方法の有用性を確かめることができた。本実行系では、音声や画像情報なども扱える。特に線描画ファイル編集では複数の作業者で同時に共同編集が行える機能を実現した。また作業者間の意志の疎通を容易にするためのサブシステム（画像や音声情報の交換機能）等を用意するなどの工夫をしている., In this paper, a groupware is treated as a distributed system where the contents and ordering of the actions in a group work are described as a service specification in an extended FSM model. In order to ensure the temporal ordering of the actions described in a service specification, each person in the group must exchange some data values and synchronization messages each other. The description of each person's work flow including both data exchanges and his own work contents is called a protocol entity specification. In this paper, we propose an algorithm for deriving the protocol entities' specifications from a service specification and a resource allocation. We have implemented the algorithm where the derived protocol entities' specifications are given as C programs and they can be executed in parallel on UNIX systems. We have also developed a system to support the group work in those protocol entities' specifications. The system has some facilities to represent sound data and pictures. The users can edit the same figure simultaneously and each modification is shown to the displays of all users where the conflicts of modifications are well solved. The system also has communication and drawing tools so that the users can exchange their ideas in the group conveniently. Our approach is useful especially for the case that the service specification and resource allocation are frequently changed.

分散システム全体の外部から観測できる動作の内容や実行順を記述した要求仕様から要求仕様どおりに動作する各ノードの動作仕様(どのようなタイミングでどのノードとどのような同期用メッセージやレジスタ値を交換しながら自ノードの動作を実行したり,自ノードのレジスタ値を更新していくべきかを記述したもの)を自動生成できることが望ましい.一方,分散システムでは,ノードやリンク故障を考慮して,これらの故障が生じても,システム全体として要求仕様どおり動くシステムの設計が望まれる.本論文では,レジスタを持つ拡張有限状態機械(EFSM)としてモデル化された分散システム全体の要求仕様から,要求仕様どおりに動作する各ノードの動作仕様(EFSM)を自動生成するための一つのアルゴリズムを提案する.この動作仕様では,高々一つのリンク故障に対して,同一メッセージを異なる2経路で送受信することにより,エラー回避が行われる.その際,単純に二重化せず同一リンクで送信される複数のメッセージを単一のメッセージに統合して,その際のノード間のメッセージ交換の総数をできるだけ少なくしている.メッセージ総数の最小化のために0-1整数線形計画問題の解法を用いている., In a distributed system, the protocol entities must exchange some data values and synchronization messages in order to ensure the temporal ordering of the events described in a service specification for the distributed system. It is desirable that a correct protocol specification can be derived automatically from a given service specification. In this paper, we propose an algorithm which synthesizes automatically a correct protocol specification from a service specification described as an extended FSM(EFSM)model. In our model, message loss is considered as the communication link errors. We assume that at most one communication link may be down. Even if all the messages in the faulty link are lost, the derived protocol specification can simulate the service specification correctly. To avoid the influences of the communicatinon errors, we use duplicated messages with the same information. In our method, however, in order to reduce the number of exchanged messages at each transition, all the messages used in the same link at each phase are merged into one message. To minimize the number of the exchanged messages, we use a procedure to calculate an optimal solution for 0-1 integer linear programming problems.

ソフトウェアプロセス全体を実働化する際,プロセスでの各作業内容とそれらの実行順序に加え,技術者間のデータの交換作業や作業間の同期を考慮する必要がある.しかし,設計者がそれらを陽に誤りなく記述することは困難であり,繁雑でもある.そこで,本稿では,ソフトウェアプロセスの(Kellnerの)標準的例題の全体をそのソフトウェアプロセスで行われる作業内容とそれらの実行順序のみで記述した.そして,その全体記述と,ソフトウェア開発に必要なファイルや文書などの各技術者への分散配置情報から,各技術者のデータの送受信も含んだ動作記述を,我々がすでに提案した導出法に従って機械的に導出した.記述モデルとして,並列動作等が扱える,レジスタを持ちデータを処理できるように拡張したペトリネットのサグクラス(FCネット)を用いる.導出した各技術者の動作記述もペトリネットモデルで記述されるため,各技術者は,どの作業がどのような順番であるいは並列に行われているかを視覚的に把握することができる.本研究により,我々が提案したモデルでソフトウェアプロセスを記述でき,それを分散制御できるような動作記述を自動導出できることが示された.これにより本手法の有用性が確かめられた., In order to enact a whole software process description,it is necessary to specify not only the contents of activities of the software process and their temporal ordering but also the communications among the engineers to synchronize or to exchange data values.However,it is very complicated for the designers to describe them correctly.In this paper,we have described only the whole description of the standard process modelling examaple problem(Kellner's example problem),where only the contents of activities of the software process and temporal ordering of the activities are specified,in an extended Petri net model with a finit number of registers which can treat data values.We have also derived each engineer's individual description including the communications among the engineers automatically from the whole description and a distributed allocation of the files and documents neceessary for the software development,using the derivation algorithm which we have already proposed.Since the derived individual descriptions are also described in the same model,each engineer can understand his, her own working flows(including parallel actions).In our research,it has shown that in our proposed model,the software processes can be described, and that we can derive the individual descriptions which can be carried out at a distributed control.The usefulness of our approach is also shown in this example.

In a distributed system, the protocol entities must exchange some data values and synchronization messages in order to ensure the temporal ordering of the events described in a service specification for the distributed system. It is desirable that a correct protocol specification can be derived automatically from a given service specification. In this paper, we propose an algorithm which synthesizes automatically a correct protocol specification from a service specification described as a Marked Graph with Registers (MGR) model and resources (registers and gates) allocation information. This model has a finite control modeled as a marked graph. Therefore, parallel events can be described. In our method, to minimize the number of the exchanged messages, we use a procedure to calculate an optimum solution for 0-1 integer linear programming problems. The number of the steps which each protocol entity needs to simulate one transition in the service specification is also minimized. Ways to avoiding conflict of registers are also described. Our approach has the following advantages. First, parallel events can be described in a service specification. Secondly, many practical systems can be described in the MGR model. Finally, at the protocol specification level, we can understand what events can be executed in parallel.

本論文では代数的手法による順序機械型プログラムの階層的設計法について提案する．我々の階層的設計法では要求仕様から実現プログラムまで同一の詳細化法に基づいて段階的に順次詳細化していく．各レベルでは，そのレベルでの関数，処理の性質等の要求記述が行われ，そのレベルで閉じた記述になっている．我々は，プログラム設計技法の共通問題として提供された在庫管理問題に対し本手法を適用し，他の文献では見られなかった入出力関係のみを指定した要求記述から，5段階にわたって逐次詳細化し，プログラムを開発した．本論文では記述の概略と共に，要求記述や詳細化の際に一般的に生じる問題点，解決法を述べ，また，他の方法論との比較も行っている．「拡張射影」と呼ばれる単純な枠組で最上位の満たすべき入出力関係を記述できること，記述は完全に階層的であること，各レベルの要求記述はいわゆるオーバスペックにならないように必要なことのみ記述していること，各レベルの要求記述に抜けがないよう記述スタイルを工夫していること，正しさの形式的な証明が可能であったこと，実現プログラムの実行時間はCプログラムのそれのたかだか2倍程度であること，等の結果より，本設計法および処理系の有効性が確かめられた．

分散システム全体の要求仕様から要求仕様通りに動作する各ノードの動作仕様(どのようなタイミングでどのノードとどのような同期用メッセージやレジスタ値を交換しながら自ノードの作動を実行したり,自ノードのレジスタ値を更新していくべきかを記述したもの)を自動生成できることが望ましい.そこで,本論文ではレジスタを持つ拡張有限状態機械(EFSM)としてモデル化された分散システム全体の要求仕様から,要求仕様通りに動作する各ノードの動作仕様(EFSM)を自動生成するためのアルゴリズムを提案する.このモデルでは,非決定性の動作が記述できる.また,入力と状態だけでなくその時点のレジスタ値に依存して次の状態や次のレジスタ値を定めることができる.各レジスタは分散システムのリソースを表すと考える.どのノードに各リソースを配置するかは設計者が決める.同一リソースを複数ノードに分散配置してもよい.作成した自動生成アルゴリズムでは,与えられた要求仕様とゲートや,リソースの配置情報から各ノードの動作仕様を自動生成する.導出は要求仕様の各状態遷移を,選択動作の通知,レジスタ値の転送,レジスタ値の更新,更新終了の通知などの一連の動作の系列で置き換えることにより実現し,0-1線形計画問題の解法を用いて,その際のノード間のメッセージ交換の総数をできるだけ少なくしている., In a distributed system, the protocol entities must exchange some data values and synchronization messages in ordar to ensure the temporal ordering of the actions described in a requirement specification for the distributed system. It is desirable that the protocol entities' specifications can be derived automatically from the requirement specification for the distributed system. ln this paper, we propose an algorithm which synthesizes automatically the protocol entities' specifications from a requirement specification described as an extended FSM (EFSM) model. The next state and values of the registers are determined depending on not only the current state and input, but also the current vaIues of the registers. In this model, we can describe nondeterministic behaviors. Each resource is treated as a register. The registers are allocated to the protocol entities. According to the allocation of the registers, each protocol entity's specification is derived. The allocation is specified by the designer. An algorithm solving 0-1 integer linear programming problems is used to reduce the number of the messages between the protocol entities.