研究者詳細 - 結縁　祥治

論文 - 結縁　祥治

分割表示 84 件中 21 - 40 件目／全件表示 >>

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月

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月

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月

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月

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.

　前のページ - 次のページ　

<結縁 祥治>

論文 - 結縁 祥治

<結縁　祥治>

論文 - 結縁　祥治