論文 - 結縁　祥治

Maude による否定を含んだ構造操作意味定義インタプリタと等価性検証器の構築

伴潤,今井敬吾,結縁祥治

電子情報通信学会技術研究報告(ソフトウェアサイエンス)   109 巻 ( 40 ) 頁： 49-54   2009年5月

　詳細を見る

記述言語：日本語  

Apache Cocoon Flowscriptのモデル検査によるWeb応用プログラムの動作検証

馬場　敬・結縁祥治・阿草清滋

信学技報SS-0903     頁： 19-24   2009年3月

　詳細を見る

担当区分：筆頭著者   記述言語：日本語  

動的電圧制御システムにおける評価戦略選択に基づく高効率消費エネルギー関数型プログラミング 査読有り

横山哲郎 今井敬吾 曾剛 冨山宏之 高田広章 結縁祥治

情報処理学会論文誌(プログラミング)   PRO41 巻 ( 2 ) 頁： 54-69   2009年3月

　詳細を見る

記述言語：日本語   掲載種別：研究論文（学術雑誌）  

Environmental simulation of real-time systems with nested interrupts in Maude 査読有り

Li Guoqiang, Shoji Yuen, and Masakazu Adachi

    頁： 133-147   2009年3月

　詳細を見る

記述言語：英語  

A full implementation of session types in Haskell 査読有り

Keigo Imai, Shoji Yuen, and Kiyoshi Agusa

    頁： 44-56   2009年3月

　詳細を見る

記述言語：英語  

*Generating priority rewrite systems for OSOS process languages 査読有り

Irek Ulidowski and Shoji Yuen

Information and Computation   207 巻 ( 2 ) 頁： 120-145   2009年2月

　詳細を見る

記述言語：英語   掲載種別：研究論文（学術雑誌）  

*充足可能性判定に基づくリアルタイムシステムのスケジューリング解析 査読有り

足立正和、末次亮、結縁祥治、手嶋茂晴、佐野範佳

組込みシステムシンポジウム2008論文集     頁： 41-49   2008年10月

　詳細を見る

記述言語：日本語  

通信指向プログラミングによる高信頼ソフトウェア設計

結縁祥治

第六回ディペンダブルシステムワークショップDSW2008論文集     頁： 135   2008年7月

　詳細を見る

担当区分：筆頭著者   記述言語：日本語  

通信プロセス計算とその時間拡張 招待有り 査読有り

結縁祥治

システム制御学会論文誌   52 巻 ( 9 ) 頁： 322-327   2008年9月

　詳細を見る

担当区分：筆頭著者   記述言語：日本語  

Communication centered programming of integrated services with priority in home appliance network 査読有り

Sakura Bhandari, Shoji Yuen, Kiyoshi Agusa

In Proceedings of APSEC2007 Workshop on Service Oriented Architecture     頁： 8-15   2007年12月

　詳細を見る

記述言語：英語  

We propose an extended framework of communication
centered programming for home appliance network where
the distributed environment is designed in the service oriented
architecture. Home appliances are now getting connected
to network. By exchanging messages over network,
various appliances constitute "integrated services"
in that the operations by the appliances are performed
as programmed. Following the communication centered
programming, a global description is directly given
for interactions that involve many appliances. A behaviorally
equivalent local description distributed for the appliances
is derived by the end-point projection(EPP). This
significantly eases the distributed system programming. The
communication centered programming is originally proposed
by Carbone et.al. Services are available at the same
time and a certain service may or must have the precedence
over the other services to be consistent. To cope with this,
we introduce "priority" in the communication centered programming.
We present a design extension for priority both
in global descriptions and local descriptions by examples.
We argue the end-point projection with priority towards the
automatic derivation of local descriptions from global descriptions.

A synchronization flow analysis of concurrent objects in AIBO OPEN-R programs based on communicating processes 査読有り

Ryo Suetsugu, Shoji Yuen, Kiyoshi Agusa

In Proceedings of 14th Asia-pacific software engineering conference APSEC2007, IEEE computer society     頁： 366-373   2007年12月

　詳細を見る

記述言語：英語  

We propose a compositional analysis method for synchronization
flow in AIBO OPEN-R programs based on
communicating processes. Concurrent objects of AIBO programs
with the OPEN-R API are synchronized by two types
of signals: ready and notify. Focusing on these signals,
we describe abstract behavior of AIBO programs in the pi-
calculus preserving the source code structure. We modelcheck
deadlock freeness and interactions order of AIBO
programs based on this abstract behavior. Since a primary
issue in model-checking is the state space explosion in the
behavioral model, we present a decomposing method to reduce
the combination of states of concurrent objects. Since
our translation to the pi-calculus preserves the syntactical
structure of source code, when a counter-example is pointed
out, our method enables not only to detect the violation of
property of the whole system, but also to point out which
component may cause the violation. We developed a prototype
translator from AIBO OPEN-R programs to abstract
description in the pi-calculus. We show that an application
of our decomposing method enables to practically modelcheck
properties by existing tools in two examples of AIBO
programs.

通信プロセスモデルによるAIBO OPEN-Rプログラムのデッドロックフリー解析手法 査読有り

末次亮、結縁祥治、阿草清滋

情報処理学会論文誌   48 巻 ( 9 ) 頁： 2915-2924   2007年9月

　詳細を見る

記述言語：日本語   掲載種別：研究論文（学術雑誌）  

本論文ではAIBOプログラムの振る舞いを通信プロセスモデルに基づいて表現し、デッドロックフリー解析を行う手法を提案する。AIBOプログラムの標準的開発環境OPEN-Rで開発された並行オブジェクトのやりとりする同期信号に基づいて制御の流れを定式化し、実行においてデッドロックのないことを示す。

分散環境における家電機器の連携動作の記述手法

バンダリさくら、結縁祥治、阿草清滋

第５回ディペンダブルシステムワークショップ論文集     頁： 35-44   2007年7月

　詳細を見る

記述言語：日本語  

セッション型に基づく高信頼性ネットワークプログラムのHaskell言語による実装

今井敬吾、結縁祥治、阿草清滋

第５回ディペンダブルシステムワークショップ論文集     頁： 95-106   2007年7月

　詳細を見る

記述言語：日本語  

π計算におけるセッションの構造化

今井敬吾、結縁祥治、阿草清滋

第９回プログラミングおよびプログラミング言語ワークショップ論文集     頁： 140-154   2007年3月

　詳細を見る

記述言語：日本語  

Haskellのための非同期局所化π計算に基づくネットワークプログラミングフレームワーク 査読有り

今井敬吾、結縁祥治、阿草清滋

情報処理学会論文誌(トランザクション)プログラミング   ( 47 ) 頁： 10,18   2006年10月

　詳細を見る

記述言語：日本語   掲載種別：研究論文（学術雑誌）  

π計算に対する時間拡張と合同的性質 査読有り

桑原 寛明, 結縁 祥治, 阿草 清滋

電子情報通信学会論文誌   J89-D 巻 ( 4 ) 頁： 632,641   2006年4月

　詳細を見る

記述言語：日本語   掲載種別：研究論文（学術雑誌）  

通信プロセスモデルと形式意味論に基づくソフトウェアのモデル化 査読有り

コンピュータソフトウェア   22 巻   頁： 22-43   2005年

　詳細を見る

担当区分：筆頭著者   記述言語：日本語  

Towards Assurign Quality Attributes of Client Dynamic Web Applications: Identifying and Addressing the Challenges 査読有り

Mohammed Sharaf Aun, Shoji Yuen, Kiyoshi Agusa

Journal of Web Engineering   4 巻   頁： 144-164   2005年

　詳細を見る

記述言語：英語   掲載種別：研究論文（学術雑誌）  

Name-passing style GUI Programming in a pi-calculus-based language Nepi 査読有り

Atsushi Mizuno, Ken Mano, Yoshinobu Kawabe, Hiroaki Kuwabara, Shoji Yuen, Kiyoshi Agusa

Electric Notes of Theoretical Computer Science   139 巻   頁： 145-168   2005年

　詳細を見る

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

This paper describes name-passing style Graphic User Interface (GUI) programming in the programming language Nepi whose operational semantics is based on the rendezvous-style name-passing communication of the π-calculus. Nepi is able to have timed behavior by combining the wait prefix with the external choice. We model GUI programs by using channel-based behavioral characterization. We propose a pair of extended syntax elements `?g' and `!g' in Nepi to generate and terminate graphic components. The graphic components are accompanied by event handling processes that convert an event to specified name-passing. In the extended Nepi, a GUI program is described as the composition of graphic components, event handling processes, and function processes that implement the real function. We present an implementation of a GUI extension for Nepi programming language on Allegro Common Lisp to illustrate the features of name-passing style GUI programming in Nepi with examples. Finally, we discuss a formal treatment and verification technique based on the extended reduction semantics of Nepi.