研究者詳細 - 結縁　祥治

写真a

ユウエン　シヨウジ

結縁　祥治

YUEN, Shoji

所属

大学院情報学研究科情報システム学専攻ソフトウェア論教授

大学院担当

大学院情報科学研究科
大学院情報学研究科

学部担当

工学部
情報学部コンピュータ科学科

連絡先

ホームページ

http://www.sqlab.jp/person/yuen/index.html

学位 2

博士(工学) （ 1997年2月名古屋大学）
工学修士（ 1987年3月京都大学）

学位の先頭へ▲

研究分野 1

その他 / その他 / 計算機科学

研究分野の先頭へ▲

現在の研究課題とSDGs 1

並行プログラムの形式的意味論

現在の研究課題とSDGsの先頭へ▲

経歴 5

名古屋大学大学院情報学研究科教授

2007年4月 - 現在

　詳細を見る

国名：日本国
名古屋大学大学院情報科学研究科准教授

2003年4月 - 2007年3月

　詳細を見る

国名：日本国
名古屋大学工学研究科助教授

2000年8月 - 2003年3月

　詳細を見る

国名：日本国
名古屋大学情報メディア教育センター助教授

1998年4月 - 2000年7月

　詳細を見る

国名：日本国
名古屋大学工学部助手

1990年4月 - 1998年3月

　詳細を見る

国名：日本国

経歴の先頭へ▲

学歴 3

名古屋大学工学研究科情報工学

1987年4月 - 1990年3月

　詳細を見る

国名：日本国
京都大学工学研究科情報工学専攻

1985年4月 - 1987年3月

　詳細を見る

国名：日本国
京都大学工学部情報工学科

- 1985年

　詳細を見る

国名：日本国

学歴の先頭へ▲

所属学協会 5

電子情報通信学会研究専門委員会委員長(ソフトウェアサイエンス)

2014年5月 - 2016年4月
情報処理学会東海支部評議員

2009年5月 - 2011年4月
日本ソフトウェア科学会学会誌編集委員

2004年4月 - 2017年3月
情報処理学会東海支部幹事

2002年4月 - 2004年3月
Association for Computer Machinary

所属学協会の先頭へ▲

委員歴 19

16th International Conference on Reversible Computation (RC) Program Committee member

2023年11月 - 2024年7月

　詳細を見る

団体区分：学協会
20th International Conference on Formal Aspects of Component Software Program Committee member

2024年3月 - 2024年11月

　詳細を見る

団体区分：学協会
PLACES 2024: 15th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software Program Committee member

2023年11月 - 2024年3月

　詳細を見る

団体区分：学協会
19th International Conference on Formal Aspects of Component Software Program Committee member

2023年4月 - 2023年11月

　詳細を見る

団体区分：学協会
Program Committee member

2022年9月 - 2023年3月

　詳細を見る

団体区分：学協会
18th international conference on Formal Aspects of Component Software Program Committee member

2022年3月 - 2022年11月

　詳細を見る

団体区分：その他
15th International Conference, Reversible Comoputation Program Committee member

2022年11月 - 2023年7月
17th International Conference on Formal Aspects of Component Software PCmember

2021年10月

　詳細を見る

団体区分：学協会
13th International Conference, Reversible Computing General Chair

2020年8月 - 2021年7月

　詳細を見る

団体区分：学協会
16th International Conference on Formal Aspects of Component Software PCmember

2019年10月

　詳細を見る

団体区分：学協会
13th International Colloquium on Theoretical Aspects of Computing PCmember

2016年11月
2014年日本ソフトウェア科学会大会 2014大会実行委員長

2014年1月 - 2014年9月

　詳細を見る

団体区分：学協会
11th International Symposium on Automated Technology for Verification and Analysis PCmember

2013年10月
23rd International Conference on Concurrency Theory PCmember

2011年9月 - 2012年9月
Structural Operational Semantics 2008 PCmember

2008年9月
6th International Symposium on Automated Technology for Verification and Analysis PCmember

2008年9月
8th International Symposium on Functional and Logic Programming General Chair

2008年5月
Structural Operational Semantics 2007 PCmember

2007年9月

　詳細を見る

団体区分：学協会
5th International Symposium on Automated Technology for Verification and Analysis PCmember

2007年9月

▼全件表示

委員歴の先頭へ▲

論文 81

revTPL: The Reversible Temporal Process Language 査読有り国際共著

Laura Bocchi ; Ivan Lanese ; Claudio Antares Mezzina ; Shoji Yuen.

Logical Method in Computer Science 20 巻 ( 1 ) 頁： 11:1 - 11:35 2024年1月

　詳細を見る

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

DOI： https://doi.org/10.46298/lmcs-20(1:11)2024
CRIL: A Concurrent Reversible Intermediate Language 査読有り

Shunya Oguchi, Shoji Yuen

Electronic Proceedings in Theoretical Computer Science 387 巻頁： 149 - 167 2023年9月

　詳細を見る

担当区分：最終著者,　責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

DOI： https://dx.doi.org/10.4204/EPTCS.387.11
可逆並行オブジェクト指向プログラミング言語：CROOPLPP

赤池佑介,結縁祥治

信学技報 123 巻頁： 13 - 18 2023年7月

　詳細を見る

担当区分：責任著者記述言語：日本語掲載種別：研究論文（研究会，シンポジウム資料等）
CRSSA: 並行可逆言語に対する静的単一代入査読有り

小口隼也, 結縁祥治

第25回プログラミングおよびプログラミング言語ワークショップ PPL 2023 頁： 1 - 20 2023年3月

　詳細を見る

担当区分：責任著者記述言語：日本語掲載種別：研究論文（研究会，シンポジウム資料等）
A reversible debugger for imparative parallel programs with contracts 査読有り

Takashi Ikeda, Shoji Yuen

Reversible Computation 2022, Lecture Notes in Computer Science 13354 巻頁： 204 - 212 2022年7月

　詳細を見る

担当区分：責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

DOI： https://doi.org/10.1007/978-3-031-09005-9_14
The reversible temporal process language 査読有り国際共著

Laura Bocchi, Ivan Lanese, Claudio Antrares Mezzina, Shoji Yuen

Proceedings of FORTE 2022, Lecture Notes in Computer Science 13273 巻頁： 31 - 49 2022年6月

　詳細を見る

担当区分：責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

DOI： https://doi.org/10.1007/978-3-031-08679-3_3
再帰的ブロック構造を持つ並列プログラムに対する可逆実行環境査読有り

池田崇志，結縁祥治

情報処理学会論文誌トランザクション 2021年11月

　詳細を見る

担当区分：責任著者記述言語：日本語掲載種別：研究論文（学術雑誌）
Multiparty Session Programming with Global Protocol Combinators(Artifact) 招待有り査読有り国際共著

Keigo Imai, Rumiyana Neykova, Nobuko Yoshida, Shoji Yuen

Dagstuhl Artifacts Series 6 巻 ( 2 ) 頁： 1 - 2 2020年11月

　詳細を見る

記述言語：英語掲載種別：研究論文（その他学術会議資料等）

DOI： 10.4230/DARTS.6.2.18
Multiparty Session Programming with Global Combinators 招待有り査読有り国際共著

Keigo Imai, Rumiyana Neykova, Nobuko Yoshida, Shoji Yuen

LIPlcs 166 巻頁： 9:1 - 9:30 2020年11月

　詳細を見る

担当区分：責任著者記述言語：英語掲載種別：研究論文（国際会議プロシーディングス）

DOI： 10.4230/LIPIcs.ECOOP.2020.9
A Reversible Runtime Environment for Parallel Programs 査読有り

Takashi Ikeda, Shoji Yuen

Reversible Computation 2020, Lecture Notes in Computer Science 12247 巻頁： 272-279 2020年7月

　詳細を見る

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

DOI： 10.1007/978-3-030-52482-1_18
Fault Diagnosis for Distributed Cooperative System Using Inducting Logic Programming 招待有り査読有り

Shuichi Sato, Yosuke Watanabe, Hiroyuki Seki, Yoshinao Ishii, Shoji Yuen

IEEE International Conference on Prognostics and Health Management, ICPHM 2020 頁： 1 - 8 2020年6月

　詳細を見る

担当区分：責任著者

DOI： 10.1109/ICPHM49022.2020.9187032
Automating Time-series Safety Analysis for Automotive Control Systems Using Weighted Partial Max-SMT 査読有り

Shuichi Sato, Shogo Hattori, Hiroyuki Seki, Yutaka Inamori, Shoji Yuen

Journal of Information Processing 28 巻頁： 124-135 2020年1月

　詳細を見る

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

DOI： 10.2197/ipsjjip.28.124
Session-ocaml: A session-based library with polarities and lenses 査読有り

Keigo Imai, Nobuko Yoshida, Shoji Yuen

Science of Computer Program 172 巻頁： 135-159 2019年3月

　詳細を見る

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

DOI： 10.1016/j.scico.2018.08.005
Reversing Event Structure 査読有り

Irek Ulidowski, Iain Phillips, Shoji Yuen

New Generation Computing 36 巻頁： 281-306 2018年9月

　詳細を見る

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

DOI： 10.1007/s00354-018-0040-8
Reversing Parallel Programs with Blocks and Procedures 査読有り

James Hoey, Irek Ulidowski, Shoji Yuen

EPTCS (EXPRESS/SOS 2018) 276 巻頁： 69-86 2018年9月

　詳細を見る

記述言語：英語

DOI： 10.4204/EPTCS.276.7
Nested Timed Automata with Invariants 査読有り

Yuwei Wang, Guoqiang Li, Shoji Yuen

Lecture Notes in Computer Science 10606 巻頁： 77-93 2017年10月

　詳細を見る

記述言語：英語

DOI： 10.1007/978-3-319-69483-2
Nested Timed Automata with Diagonal Constraints 査読有り

Yuwei Wang, Yunqing Wen, Guoqiang Li, Shoji Yuen

Lecture notes in computer science 10610 巻頁： 396-412 2017年11月

　詳細を見る

記述言語：英語

DOI： 10.1007/978-3-319-68690-5_24
Reversing Imperative Parallel Programs. 査読有り

James Hoey, Irek Ulidowski, Shoji Yuen

Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics and 14th Workshop on Structural Operational Semantics, EXPRESS/SOS 2017, Berlin, Germany, 4th September 2017. EPTCS 255, 2017 2017年9月

　詳細を見る

記述言語：英語

DOI： 10.4204/EPTCS.255.4
Session-ocaml: A Session-Based Library with Polarities and Lenses 査読有り

Keigo Imai, Nobuko Yoshida, Shoji Yuen

Lecture Notes in Computer Science 10319 巻頁： 99-118 2017年6月

　詳細を見る

記述言語：英語

DOI： 10.1007/978-3-319-59746-1_6
Automating Time Series Safety Analysis for Automotive Control Systems in STPA Using Weighted Partial Max-SMT 査読有り

Shuichi Sato, Shogo Hattori, Hiroyuki Seki,Yutaka Inamori,Shoji Yuen

Communications in Computer and Information Science ( 694 ) 頁： 39-54 2016年11月

　詳細を見る

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

DOI： 10.1007/978-3-319-53946-1_3
An Over-Approximation Forward Analysis for Nested Timed Automata 査読有り

Yunqing Wen, Guoqiang Li, Shoji Yuen

Lecture Notes in Computer Science 8979 巻頁： 1-15 2015年1月

　詳細を見る

記述言語：英語掲載種別：研究論文（学術雑誌）
Nested Timed Automata with Frozen Clocks 査読有り

Guoqiang Li, Mizuhito Ogawa, Shoji Yuen

Lecture Notes in Computer Science 9268 巻頁： 189-205 2015年9月

　詳細を見る

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

A nested timed automaton (NeTA) is a pushdown system whose control locations and stack alphabet are
timed automata (TAs). A control location describes a working TA, and the stack presents a pile of
interrupted TAs. In NeTAs, all local clocks of TAs proceed uniformly also in the stack. This paper extends
NeTAs with frozen local clocks (NeTA-Fs). All clocks of a TA in the stack can be either frozen or
proceeding when it is pushed. A NeTA-F also allows global clocks adding to local clocks in the working
TA, which can be referred and/or updated from the working TA. We investigate the reachability of NeTAFs
showing that (1) the reachability with a single global clock is decidable, and (2) the reachability with
multiple global clocks is undecidable.
Concurrency and reversibility 招待有り査読有り

Irek Ulidowski, Iain Phillips and Shoji Yuen

Reversible Computation 2014, LNCS 8507 ( 8507 ) 頁： 1-14 2014年7月

　詳細を見る

記述言語：英語掲載種別：研究論文（学術雑誌）
値付きタスクオートマトンに基づくコストを意識した実時間タスクスケジューリング

結縁祥冶、亀井達朗

信学技報 114 巻 ( 127 ) 頁： 37-42 2014年7月

　詳細を見る

担当区分：筆頭著者記述言語：日本語掲載種別：研究論文（学術雑誌）
離散事象システムにおけるMaxSATソルバを用いた最大可制御部分仕様の導出

廣田樹、結縁祥冶、東道徹也

信学技報 114 巻 ( 271 ) 頁： 35-40 2014年10月

　詳細を見る

記述言語：日本語掲載種別：研究論文（学術雑誌）
部分観測におけるMaxSATソルバを用いたスーパバイザ合成手法

廣田樹、結縁祥冶、東道徹也

信学技報 114 巻 ( 416 ) 頁： 79-84 2015年1月

　詳細を見る

記述言語：日本語掲載種別：研究論文（学術雑誌）
Modelling of Bonding with Process and Events 査読有り

Iain Phillips, Irek Ulidowski, Shoji Yuen

Lecture Notes in Computer Science 7948 巻頁： 141-154 2013年7月

　詳細を見る

記述言語：英語
Modelling and analysis of real-time systems with mutex components 査読有り

Guoqiang Li, Xiaojuan Cai, Shoji Yuen

International Journal of Foundations of Computer Science 25 巻 ( 4 ) 頁： 831-851 2012年6月

　詳細を見る

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

DOI： 10.1142/S0129054112400382
A Reversible Process Calculus and the Modelling of the ERK signalling pathway 査読有り

Iain Phillips, Irek Ulidowski and Shoji Yuen

In Proceedings of the 4th workshop on reversible computation RC2012 頁： 227-239 2012年7月

　詳細を見る

記述言語：英語
A session type systems with subject reduction 査読有り

Keigo Imai, Shoji Yuen, and Kiyoshi Agusa

IEICE Transaction, Infromatoin adn systems E95-D 巻 ( 8 ) 頁： 2053--2064 2012年8月

　詳細を見る

記述言語：英語掲載種別：研究論文（学術雑誌）
タスクマイグレーション機能を持つマルチコアスケジューリング解析

中堂園貴幸,結縁祥治

信学技法 112 巻 ( 458 ) 頁： 103-108 2013年3月

　詳細を見る

記述言語：英語掲載種別：研究論文（学術雑誌）
名前渡しプロセス計算における優先度ガード査読有り

結縁祥治, 太田正悟

プログラミングおよびプログラミング言語ワークショップ頁： 246-257 2011年3月

　詳細を見る

担当区分：筆頭著者記述言語：日本語
Modeling and Analysis of Real -Time Systems with Mutex Components 査読有り

Guoqiang Li, Xiaojuan Cai, Shoji Yuen

Advances in Parallel and Distributed Computing Models ( 3 ) 頁： 1-8 2010年4月

　詳細を見る

記述言語：英語
Session Type Inference in Haskell 査読有り

Keigo Imai, Shoji Yuen, Kiyoshi Agusa

PLACES '10: Programming Language Approaches to Concurrency and Communication-cEntric Software 頁： 43-52 2010年3月

　詳細を見る

記述言語：英語
コレオグラフィに基づく高信頼通信指向GUIプログラミング

下村翔結縁祥治

電子情報通信学会技術研究報告(ソフトウェアサイエンス) 109 巻 ( 456 ) 頁： 127-132 2010年3月

　詳細を見る

記述言語：日本語
計算資源へのアクセス能力に基づく競合検査とデッドロック検査のための型解析

坂野吉隆結縁祥治

電子情報通信学会技術研究報告(ソフトウェアサイエンス) 109 巻 ( 456 ) 頁： 133-138 2010年3月

　詳細を見る

記述言語：日本語
Environmental Simulation of Real -Time Systems with Nested Interrupts 査読有り

Guoqiang Li, Shoji Yuen, Masakazu Adachi

Theoretical Aspect of Software Engineering, TASE2009 頁： 21-28 2009年7月

　詳細を見る

記述言語：英語

Interrupts are important aspects of real-time embedded
systems to handle events in time. When there exist nested
interrupts in a real-time system, and an urgent interrupt is
allowed to preempt the current interrupt handling, the design
and analysis of the system become difficult due to the lack
of appropriate behavioral models. This paper proposes a
compositional model for nested interrupts and an analysis
named environmental simulation. We present a new kind of
timed transition system, named controller automata, to treat
interrupts. Together with an interrupt environment modeled
as a timed automaton, and a scheduler as a timed automaton
with semaphores, the system behaviors with nested interrupts
are realized by a sequence of transitions with time. Although
various verification problems for this model are undecidable
in general, it is shown that the reachability of error states
is practically solvable with our implementation of the environmental
simulation by Maude.
Maude による否定を含んだ構造操作意味定義インタプリタと等価性検証器の構築

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

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

　詳細を見る

記述言語：日本語
Apache Cocoon Flowscriptのモデル検査によるWeb応用プログラムの動作検証

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

信学技報SS-0903 頁： 19-24 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月

　詳細を見る

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

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

情報処理学会論文誌(プログラミング) PRO41 巻 ( 2 ) 頁： 54-69 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年

　詳細を見る

担当区分：筆頭著者記述言語：日本語
*Web Automata: A Behavioral Model of Web Applications based on the MVC 査読有り

Shoji Yuen, Keishi Kato, Daiju Kato, Kiyoshi Agusa

Computer Software 22 巻頁： 44-57 2005年

　詳細を見る

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

We propose a behavioral model of web applications
based on the MVC(Model View and Control)
model architecture. The MVC model architecture
separates design concerns to improve the overall
software quality. Since the architecture defines the
abstract outline of the configurations, there is a
broad gap between coding web applications and its
behavioral property.
We propose a behavioral model, called 'Web Automata',
to implement the MVC architecture. We
model the behavior of a web application with dynamic
contents as an extension of links-automata
proposed by Stotts et.al. As extended in the model
checking techniques, we view a web application as a
data-independent system, where variables appearing
in link parameters and form inputs are attached
to each page.
We propose a testing framework for web applications
based on the behavioral model. We show it
provides testing criteria for web applications when
we focus on the loops on the behavior automata.
We apply our framework to the Jakarta Struts by
presenting the extended configuration schema of
Struts in order to describe the web automata directly.
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.
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年

　詳細を見る

記述言語：英語掲載種別：研究論文（学術雑誌）
通信プロセスモデルに基づく並行オブジェクト指向言語によるAIBOプログラムの動作記述査読有り

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

ソフトウェア工学の基礎ワークショップFOSE2005 頁： 267-276 2005年11月

　詳細を見る

記述言語：日本語
*Process languages with discrete relative time based on the Ordered SOS format and rooted eager bisimulation 査読有り

Irek Ulidowski, Shoji Yuen

The Journal of Logic and Algebraic Programming 60-61 巻頁： 401-460 2004年12月

　詳細を見る

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

We propose a uniform framework, based on the Ordered Structural Operational Semantics (OSOS)
approach of Ulidowski and Phillips [Information and Computation 178 (1) (2002) 180], for process
languages with discrete relative time. Our framework allows the user to select favourite process
operators, whether they are standard operators or new application-specific operators, provided that
they are OSOS definable and their OSOS rules satisfy several simple conditions. The obtained timed
process languages preserve a timed version of rooted eager bisimulation preorder and the time determinacy
property. We also propose several additional conditions on the type of OSOS definitions for
the operators so that several other properties which reflect the nature of time passage, such as the
maximal progress, patience and time persistence properties, are also satisfied.
Name-passing style GUI programming in the π-calculus-based language Nepi 査読有り

ARTS2004(6th AMAST Workshop on Real-Time Systems)Technical Report University of Leicester ( 2004/28 ) 頁： 49-66 2004年

　詳細を見る

担当区分：筆頭著者記述言語：英語
An Approach for Debugging Client Dynamic Web Applications 査読有り

Mohammed Sharaf Aun, Shoji Yuen, Kiyoshi Agusa

45 巻頁： 2373-2383 2004年

　詳細を見る

記述言語：英語掲載種別：研究論文（学術雑誌）
FCDG に基づいたコーディングパターン査読有り

コンピュータソフトウェア 21 巻 ( 4 ) 頁： 27-36 2004年

　詳細を見る

記述言語：日本語掲載種別：研究論文（学術雑誌）
時間付きπ計算によるリアルタイムオブジェクト指向言語の形式的記述査読有り

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

情報処理学会論文誌 45 巻 ( 6 ) 頁： 1498-1507 2004年

　詳細を見る

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

組み込みシステムなどのプログラミングに用いられるオブジェクト指向言語の時間特性を形式的に記述することによってその振る舞いをできるだけ精密に特徴づけた。π計算に時間経過を導入するによって、オブジェクトの時間的振る舞いを定式化する。このことによって、小規模な実時間システムのプログラムの検証の直接的な基盤モデルを確立した。
π計算に対する時間拡張と代数的意味論査読有り

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

ソフトウェア工学の基礎ワークショップFOSE2004 頁： 97-108 2004年11月

　詳細を見る

記述言語：日本語
時間オートマトンの遷移制約記述に基づくAIBOプログラムスケルトンコードの生成手法査読有り

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

組込みソフトウェアシンポジウム2004 頁： 126-133 2004年10月

　詳細を見る

記述言語：日本語
Testing Framework for Web Applications based on the MVC model with Behavioral Description 査読有り

Shoji Yuen, Keishi Kato, Daiju Kato, Shinichiro Yamamoto, Kiyoshi Agusa

Proceedings of ICITA 頁： 11-4:1-6 2004年1月

　詳細を見る

担当区分：筆頭著者記述言語：英語
実行可能なメモリモデルに基づくJava並行プログラムのモデル検査査読有り

深谷直彦、結縁祥治、阿草清滋

ソフトウェア工学の基礎ワークショップFOSE2003 頁： 227-238 2003年11月

　詳細を見る

記述言語：日本語
時間つきπ計算によるリアルタイムオブジェクト指向言語の形式的記述査読有り

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

オブジェクト指向最前線頁： 69-76 2003年8月

　詳細を見る

記述言語：日本語
Process Languages for Rooted Weak Preorders

Irek Ulidowski, Shoji Yuen

Technical Report , University of Leicester 2002 巻 ( 11 ) 2002年

　詳細を見る

記述言語：英語掲載種別：研究論文（大学，研究機関等紀要）
NATによる準マルチホーム化技法査読有り

梶田将司、結縁祥治

情報処理学会論文誌 42 巻 ( 12 ) 2001年

　詳細を見る

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

本論文では、ネットワークの基幹に属さない任意の規模のネットワークが局所的なポリシーに基づいて複数のインターネット接続を行う方法を提案する。本手法では、NAT(ネットワークアドレス変換)を用いて複数の外部ネットワークをプライベートネットワークにマッピングすることによる複数接続を実現する。本技法によるマルチホーム化は、ネットワークが異なる複数のグローバルアドレスを用い、接続する側の利用者が通信先に応じて経路を選択することで、一方的に信頼性、効率の向上をもk的とするため、通常のマルチホーム化と区別し、準マルチホーム化と呼ぶ。準マルチホーム化によって、複数の対外接続を局所的なポリシーに基づいて制御することができるようになるため、実際の運営形態に応じた柔軟な負荷の分散と接続の確保が可能になる。最後に名古屋大学情報メディア教育センターにおける本技法の実現方法および評価を示す。
Timed Properties for Process Languages with Time 査読有り

Irek Ulidowski and Shoji Yuen

In Proceedings of SCI2001, Volume XIV 頁： 344-349 2001年

　詳細を見る

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

We present a uniform framework for defining timed process languages
based on the OSOS(Ordered Structural Operational Semantics)
approach
proposed by Ulidowski and Phillips. Our aim is
to develop a general method for extending arbitrary process
languages with temporal actions. An application of this
method to a process language, for example CCS or CSP,
produces an extension of the language with additional process
operators and the notion of time that are most suitable
a task in hand. We review several important properties of
time passage, for example time determinacy,
and propose several syntactic conditions which
guarantee these properties in a process language
with time.
General Process Languages with Time

Irek Ulidowski, Shoji Yuen

Technical Report, University of Leicester 2000 巻 ( 41 ) 2000年

　詳細を見る

記述言語：英語掲載種別：研究論文（大学，研究機関等紀要）
Process Languages for Rooted Eager Bisimulation 査読有り

Lecture Notes in Computer Science 1877 巻頁： 275,289 2000年8月

　詳細を見る

記述言語：英語
*Testing Theory for Probabilistic Processes 査読有り

Rance Cleaveland, Zeynep Dayar, Scott Smolka, Shoji Yuen

Information and Computation 154 巻頁： 93-148 1999年

　詳細を見る

記述言語：英語掲載種別：研究論文（学術雑誌）
正則な実時間通信プロセスに対するテスト擬順序の記号的特性化

電子情報通信学会論文誌 J80-D-1 巻 ( 6 ) 頁： 474-485 1997年

　詳細を見る

担当区分：筆頭著者記述言語：日本語掲載種別：研究論文（学術雑誌）
Extending Process Language with Time 査読有り

Lecture Notes In Computer Science 1349 巻 1997年

　詳細を見る

担当区分：筆頭著者記述言語：英語
Fully Abstract Characterizations of Testing Preorders for Probabilistic Processes 査読有り

Lecture Notes in Computer Science 836 巻頁： 497-512 1994年

　詳細を見る

担当区分：筆頭著者記述言語：英語
An extension of the testing method for processes passing infinite values 査読有り

Shoji Yuen, Toshiki Sakabe, Yasuyoshi Inagaki

Workshop in Computing 頁： 155-173 1993年

　詳細を見る

担当区分：筆頭著者記述言語：英語掲載種別：研究論文（学術雑誌）
An Extension of the Testing Method for Processes Passing Infinite Values 査読有り

The John Hopkins University 頁： 10:1-20 1992年8月

　詳細を見る

担当区分：筆頭著者記述言語：英語
CCSによるモニタ記述の形式的記述査読有り

結縁祥治、坂部俊樹、稲垣康義

電子情報通信学会論文誌 J73-D-1 巻頁： 683-692 1990年

　詳細を見る

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

▼全件表示

論文の先頭へ▲

書籍等出版物 2

理論計算機科学事典査読有り

結縁祥治（担当：分担執筆 , 範囲: 6.4 並行計算）

朝倉書店 2022年1月

　詳細を見る

総ページ数：807 担当ページ：586-603 記述言語：中国語著書種別：事典・辞書
並行プロセスの操作的および代数的意味論

稲垣康義、結縁祥治（担当：共著）

丸善 1993年

　詳細を見る

記述言語：日本語

書籍等出版物の先頭へ▲

講演・口頭発表等 9

Nested Timed Automataに対するZoneに基づく到達可能性解析

城聖一郎,小川瑞史,結縁祥治

電子情報通信学会ソフトウェアサイエンス研究会 2024年3月7日電子情報通信学会

　詳細を見る

開催年月日： 2024年3月

記述言語：日本語会議種別：口頭発表（一般）

開催地：石垣市健康福祉センター国名：日本国
Bidirectional Flow analysis for a concurrent reversible programming language

Shoji Yuen

2024年2月28日

　詳細を見る

開催年月日： 2024年2月

記述言語：英語会議種別：公開講演，セミナー，チュートリアル，講習，講義等

開催地：University of Urbino, Italy 国名：イタリア共和国

We present bidirectional data flow analysis for constant propagation
in the concurrent reversible intermediate language, CRIL, proposed by
the authors. A CRIL program is a collection of basic blocks. Each
basic block consists of one 3-address code with labels for forward and
backward control flow. CRIL extends RIL, proposed by Mogensen,
allowing the multiple calls of basic blocks to execute concurrently in
forward and backward directions. The operational semantics enjoy
causal safety and causal liveness as the fundamental correctness for
reversibility.

We present a bidirectional flow analysis for CRIL programs by
constructing a control flow graph for a CRIL program with possible
data flow between threads via shared variables. It is shown that the
forward and backward data flow edges cover all the data flows in
executing the program in either direction. Based on the flow
analysis, we further propose a syntactic translation to SSA forms with
reversibility for optimizing CRIL programs. We propose the method for
constant propagation and common sub-expression elimination.

その他リンク： https://www.uniurb.it/novita-ed-eventi/5685
Constant Propagation in CRIL by Bidirectional Data Flow Analysis

Shunya Oguchi and Shoji Yuen

2024年1月11日

　詳細を見る

開催年月日： 2024年1月

記述言語：英語会議種別：口頭発表（一般）

国名：日本国

We present bidirectional data flow analysis for constant propagation in the concurrent reversible intermediate
language, CRIL, proposed by the authors. A CRIL program consists of basic blocks, each with one instruction
enclosed by entry and exit labels. In CRIL, basic blocks are executed concurrently in forward and backward directions,
keeping causal safety and causal liveness as the fundamental correctness for reversibility. To optimize CRIL programs,
we focus on bidirectional data flow among basic blocks. We propose data flow analysis among basic blocks to reveal
data flow conflicts in both directions. The bidirectional data flow analysis enables the backward constant propagation
in addition to the forward one. We define directed edges labeled variables among basic blocks for possible forward
data flows and give directed edges for possible backward data flows using the edges of foward data flows. It is shown
that the forward and backward data flow edges cover all the data flows in executing the program in either direction.
Based on this soundness property, if a constant propagates by the data flow edges, then it propagates in all concurrent
executions of both directions. We show bidirectional constant propagation in a CRIL example by the data flow
analysis.
充足可能性判定を利用した実現可能な時間オートマトンの検証

城　聖一郎,結縁祥治

電子情報通信学会ソフトウェアサイエンス研究会 2022年7月29日電子情報通信学会

　詳細を見る

開催年月日： 2022年7月

記述言語：日本語会議種別：口頭発表（一般）

開催地：札幌市国名：日本国
通信プロセスに対する文脈変換手法を用いたモデル検査

木川泰夫、結縁祥治、坂部俊樹

電子情報通信学会コンピュテーション研究会

　詳細を見る

開催年月日： 1999年

記述言語：日本語会議種別：口頭発表（一般）

国名：日本国

電子情報通信学会技術報告COMP98-82, pp.25-32
時間オートマトンによる振舞いモデルに基づく高信頼Real-time Javaコード生成手法

井上公博、結縁祥治、阿草清滋

電子情報通信学会ソフトウェアサイエンス研究会

　詳細を見る

開催年月日： 2005年3月

記述言語：日本語会議種別：口頭発表（一般）

国名：日本国
Communication Centered Programming of Integrated Services with Priority in Home Appliance Network 国際会議

BASICS 2009 International Workshop on Computation and Interaction, Shianghai Jiao Tong University

　詳細を見る

開催年月日： 2009年10月

記述言語：英語会議種別：口頭発表（一般）

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 interactio
Session types in OCaml 国際会議

Keigo Imai, Nobuko Yoshida, Shoji Yuen

Theory and Applications of Behavioural Types (Dagstuhl Seminar 17051)

　詳細を見る

開催年月日： 2017年1月 - 2017年2月

記述言語：英語会議種別：口頭発表（一般）

国名：ドイツ連邦共和国
タスクマイグレーション機能を持つマルチコアスケジューリング解析

中堂園貴幸, 結縁祥治

電子情報通信学会ソフトウェアサイエンス研究会

　詳細を見る

開催年月日： 2013年3月

記述言語：日本語会議種別：口頭発表（一般）

国名：日本国

▼全件表示

講演・口頭発表等の先頭へ▲

共同研究・競争的資金等の研究課題 4

実用上効率的な振舞いに基づくソフトウェア検証の数理的構造

2015年3月 - 2017年12月

二国間交流事業共同研究

　詳細を見る

資金種別：競争的資金
高信頼車載システムの検証手法の研究

2007年4月 - 2009年3月

国内共同研究

　詳細を見る

車載ソフトウェアの不具合を開発段階で発見することをねらいとして，形式手法を取り入れた設計方法論と検証手法を開発する。具体的には，組込みソフトウェアにおける外部からの割込みの影響を含めて，タスクスケジューラビリティを解析する手法を開発する．
Webアプリケーション指向ソフトウェアモデリング

2002年11月 - 2006年3月

科学技術振興機構　さきがけ研究

　詳細を見る

資金種別：競争的資金

Webアプリケーションの意味論の基礎を成す形式体系、さらに、これらに基づいて提案されている言語、形式モデルとは独立に提案されている言語などを検討し、新たな計算モデルの形式化を行う。
構造的操作意味定義に基づく実時間並行ソフトウェアの振舞い解析に関する研究

2001年 - 2002年

日本学術振興会

　詳細を見る

資金種別：競争的資金

共同研究・競争的資金等の研究課題の先頭へ▲

科研費 2

コレオグラフィ記述に基づく組込みシステムの高信頼性設計技法

2007年

科学研究費補助金基盤研究（Ｃ）（一般），課題番号：19500026

結縁　祥治

　詳細を見る

担当区分：研究代表者
データと時間を扱うオートマトンネットワークの合成的アクティブ学習に基づく設計手法

研究課題/研究課題番号：21H03415 2021年4月 - 2026年3月

日本学術振興会基盤研究(B)

　詳細を見る

担当区分：研究代表者資金種別：競争的資金

配分額：17030000円（直接経費：13100000円、間接経費：3930000円）

科研費の先頭へ▲

産業財産権 1

ウィジェット操作方法、装置、プログラムおよびこのプログラムを記録した記録媒体

真野健、河辺義信、水野敦、桑原寛明、結縁祥治、阿草清滋

　詳細を見る

出願人：日本電信電話株式会社

出願番号：特願2004-165578 出願日：2004年6月

出願国：国内

産業財産権の先頭へ▲

担当経験のある科目 (本学) 4

基礎セミナーＡ

2011
知的インタフェース学特論

2001
計算機リテラシおよびプログラミング

2001
計算機基礎数理

2000

担当経験のある科目 (本学)の先頭へ▲

担当経験のある科目 (本学以外) 1

情報工学概論

2006年4月 - 2007年3月（名城大学）

担当経験のある科目 (本学以外)の先頭へ▲