Faculty Profiles - YUEN, Shoji

Papers - YUEN, Shoji

Division display 41 - 60 of about 85 ／ All the affair displays >>

Environmental Simulation of Real -Time Systems with Nested Interrupts Reviewed

Guoqiang Li, Shoji Yuen, Masakazu Adachi

Theoretical Aspect of Software Engineering, TASE2009 page： 21-28 2009.7

Language：English

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.

An SOS interpreter with negative premises andan equivalence checker by Maude

Jun BAN, Keigo IMAI, Shoji YUEN

Vol. 109 ( 40 ) page： 49-54 2009.5

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

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

信学技報SS-0903 page： 19-24 2009.3

Energy Efficient Functional Programing on DVS Systemsby Varying Evaluation Strategies Reviewed Open Access

Tetsuo Yokoyama, Keigo Imai,y1 Gang Zeng,y1Hiroyuki Tomiyama,y1 Hiroaki Takaday1and Shoji Yueny1

Vol. PRO41 ( 2 ) page： 54-69 2009.3

Environmental simulation of real-time systems with nested interrupts in Maude Reviewed

Li Guoqiang, Shoji Yuen, and Masakazu Adachi

page： 133-147 2009.3

A full implementation of session types in Haskell Reviewed

Keigo Imai, Shoji Yuen, and Kiyoshi Agusa

page： 44-56 2009.3

*Generating priority rewrite systems for OSOS process languages Reviewed

Irek Ulidowski and Shoji Yuen

Information and Computation Vol. 207 ( 2 ) page： 120-145 2009.2

Schedulability analysis of real-time systems using propositional satisfiablity Reviewed

Masakazu Adachi, Ryo Suetsugu, Shoji Yuen, Shigeharu Teshima, Noriyoshi Sano

Embedded Systems Symposium 2008 page： 41-49 2008.10

Dependable software design based on communication centered programming

Shoji Yuen

DSW2008 page： 135 2008.7

Communicating Processes with Timed Behavioral Extension Invited Reviewed Open Access

Shoji Yuen

Systems, Control and Information Vol. 52 ( 9 ) page： 322-327 2008.9

Communication centered programming of integrated services with priority in home appliance network Reviewed

Sakura Bhandari, Shoji Yuen, Kiyoshi Agusa

In Proceedings of APSEC2007 Workshop on Service Oriented Architecture page： 8-15 2007.12

Language：English

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 Reviewed

Ryo Suetsugu, Shoji Yuen, Kiyoshi Agusa

In Proceedings of 14th Asia-pacific software engineering conference APSEC2007, IEEE computer society page： 366-373 2007.12

Language：English

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.

DOI： 10.1109/ASPEC.2007.70

A Deadlock free analysis for AIBO OPEN-R programs based on communicating processes Reviewed Open Access

Ryo Suetsugu, Shoji Yuen, Kiyoshi Agusa

IPSJ Journal Vol. 48 ( 9 ) page： 2915-2924 2007.9

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

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

第５回ディペンダブルシステムワークショップ論文集 page： 35-44 2007.7

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

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

第５回ディペンダブルシステムワークショップ論文集 page： 95-106 2007.7

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

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

第９回プログラミングおよびプログラミング言語ワークショップ論文集 page： 140-154 2007.3

A Network Programming Framework in Haskell Based on Asynchronous Localized pi-calculus Reviewed

Keigo Imai, Shoji Yuen, Kiyoshi Agusa

IPSJ Transaction:Programming ( 47 ) page： 10,18 2006.10

π計算に対する時間拡張と合同的性質 Reviewed Open Access

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

電子情報通信学会論文誌 Vol. J89-D ( 4 ) page： 632,641 2006.4

通信プロセスモデルと形式意味論に基づくソフトウェアのモデル化 Reviewed Open Access

コンピュータソフトウェア Vol. 22 page： 22-43 2005

*Web Automata: A Behavioral Model of Web Applications based on the MVC Reviewed Open Access

Shoji Yuen, Keishi Kato, Daiju Kato, Kiyoshi Agusa

Computer Software Vol. 22 page： 44-57 2005

Authorship：Lead author Language：English Publishing type：Research paper (scientific journal)

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.

DOI： 10.11309/jssst.22.2_44

Open Access

　 PREV - NEXT 　

<YUEN, Shoji>

Papers - YUEN, Shoji