Updated on 2024/03/12

写真a

 
YUEN, Shoji
 
Organization
Graduate School of Informatics Department of Computing and Software Systems 3 Professor
Graduate School
Graduate School of Information Science
Graduate School of Informatics
Undergraduate School
School of Engineering
School of Informatics Department of Computer Science
Title
Professor
Contact information
メールアドレス

Degree 2

  1. Doctor of Engineering ( 1997.2   Nagoya University ) 

  2. Master of Engineering ( 1987.3   Kyoto University ) 

Research Areas 1

  1. Others / Others  / Computer Science

Current Research Project and SDGs 1

  1. Formal Semantics for Concurrent Programs

Research History 5

  1. Nagoya University   Graduate school of Informatics   Professor

    2007.4

      More details

    Country:Japan

  2. Nagoya University   Graduate School of Information Science   Associate professor

    2003.4 - 2007.3

      More details

    Country:Japan

  3. Nagoya University   Graduate School of Engineering   Associate Professor

    2000.8 - 2003.3

      More details

    Country:Japan

  4. Nagoya University   Center for Information Media Studies   Associate Professor

    1998.4 - 2000.7

      More details

    Country:Japan

  5. Nagoya University   School of Engineering   Assistant

    1990.4 - 1998.3

      More details

    Country:Japan

Education 3

  1. Nagoya University   Graduate School of Engineering   Department of Information Engineering

    1987.4 - 1990.3

      More details

    Country: Japan

  2. Kyoto University   Graduate School, Division of Engineering   Information Science

    1985.4 - 1987.3

      More details

    Country: Japan

  3. Kyoto University   Faculty of Engineering   Department of Information Science

    - 1985

      More details

    Country: Japan

Professional Memberships 5

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

    2014.5 - 2016.4

  2. 情報処理学会   東海支部評議員

    2009.5 - 2011.4

  3. Japanese Society of Software Science and Technology   Journal Editor

    2004.4 - 2017.3

  4. Information Processing Society of Japan   Organizer, Tokai-Branch

    2002.4 - 2004.3

  5. Association for Computer Machinary

Committee Memberships 19

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

    2023.11 - 2024.7   

      More details

    Committee type:Academic society

  2. 20th International Conference on Formal Aspects of Component Software   Program Committee member  

    2024.3 - 2024.11   

      More details

    Committee type:Academic society

  3. PLACES 2024: 15th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software   Program Committee member  

    2023.11 - 2024.3   

      More details

    Committee type:Academic society

  4. 19th International Conference on Formal Aspects of Component Software   Program Committee member  

    2023.4 - 2023.11   

      More details

    Committee type:Academic society

  5.   Program Committee member  

    2022.9 - 2023.3   

      More details

    Committee type:Academic society

  6. 18th international conference on Formal Aspects of Component Software   Program Committee member  

    2022.3 - 2022.11   

      More details

    Committee type:Other

  7. 15th International Conference, Reversible Comoputation   Program Committee member  

    2022.11 - 2023.7   

  8. 17th International Conference on Formal Aspects of Component Software   PCmember  

    2021.10   

      More details

    Committee type:Academic society

  9. 13th International Conference, Reversible Computing   General Chair  

    2020.8 - 2021.7   

      More details

    Committee type:Academic society

  10. 16th International Conference on Formal Aspects of Component Software   PCmember  

    2019.10   

      More details

    Committee type:Academic society

  11. 13th International Colloquium on Theoretical Aspects of Computing   PCmember  

    2016.11   

  12. 2014年日本ソフトウェア科学会大会   2014大会実行委員長  

    2014.1 - 2014.9   

      More details

    Committee type:Academic society

  13. 11th International Symposium on Automated Technology for Verification and Analysis   PCmember  

    2013.10   

  14. 23rd International Conference on Concurrency Theory   PCmember  

    2011.9 - 2012.9   

  15. Structural Operational Semantics 2008   PCmember  

    2008.9   

  16. 6th International Symposium on Automated Technology for Verification and Analysis   PCmember  

    2008.9   

  17. 8th International Symposium on Functional and Logic Programming   General Chair  

    2008.5   

  18. Structural Operational Semantics 2007   PCmember  

    2007.9   

      More details

    Committee type:Academic society

  19. 5th International Symposium on Automated Technology for Verification and Analysis   PCmember  

    2007.9   

▼display all

 

Papers 81

  1. revTPL: The Reversible Temporal Process Language Reviewed International coauthorship

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

    Logical Method in Computer Science   Vol. 20 ( 1 ) page: 11:1 - 11:35   2024.1

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

    DOI: https://doi.org/10.46298/lmcs-20(1:11)2024

  2. CRIL: A Concurrent Reversible Intermediate Language Reviewed

    Shunya Oguchi, Shoji Yuen

    Electronic Proceedings in Theoretical Computer Science   Vol. 387   page: 149 - 167   2023.9

     More details

    Authorship:Last author, Corresponding author   Language:English   Publishing type:Research paper (international conference proceedings)  

    DOI: https://dx.doi.org/10.4204/EPTCS.387.11

  3. CROOPLPP : A Reversible Concurrent Object-oriented Programming Language

    Yusuke Akaike, Shoji Yuen

      Vol. 123   page: 13 - 18   2023.7

     More details

    Authorship:Corresponding author   Language:Japanese   Publishing type:Research paper (conference, symposium, etc.)  

  4. CRSSA: 並行可逆言語に対する静的単一代入 Reviewed

    小口隼也, 結縁祥治

    第25回プログラミングおよびプログラミング言語ワークショップ PPL 2023     page: 1 - 20   2023.3

     More details

    Authorship:Corresponding author   Language:Japanese   Publishing type:Research paper (conference, symposium, etc.)  

  5. A reversible debugger for imparative parallel programs with contracts Reviewed

    Takashi Ikeda, Shoji Yuen

    Reversible Computation 2022, Lecture Notes in Computer Science   Vol. 13354   page: 204 - 212   2022.7

     More details

    Authorship:Corresponding author   Language:English   Publishing type:Research paper (international conference proceedings)  

    DOI: https://doi.org/10.1007/978-3-031-09005-9_14

  6. The reversible temporal process language Reviewed International coauthorship

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

    Proceedings of FORTE 2022, Lecture Notes in Computer Science   Vol. 13273   page: 31 - 49   2022.6

     More details

    Authorship:Corresponding author   Language:English   Publishing type:Research paper (international conference proceedings)  

    DOI: https://doi.org/10.1007/978-3-031-08679-3_3

  7. A reversible runtime for parallel programs with recursive blocks Reviewed

        2021.11

     More details

    Authorship:Corresponding author   Language:Japanese   Publishing type:Research paper (scientific journal)  

  8. Multiparty Session Programming with Global Protocol Combinators(Artifact) Invited Reviewed International coauthorship

    Keigo Imai, Rumiyana Neykova, Nobuko Yoshida, Shoji Yuen

    Dagstuhl Artifacts Series   Vol. 6 ( 2 ) page: 1 - 2   2020.11

     More details

    Language:English   Publishing type:Research paper (other academic)  

    DOI: 10.4230/DARTS.6.2.18

  9. Multiparty Session Programming with Global Combinators Invited Reviewed International coauthorship

    Keigo Imai, Rumiyana Neykova, Nobuko Yoshida, Shoji Yuen

    LIPlcs   Vol. 166   page: 9:1 - 9:30   2020.11

     More details

    Authorship:Corresponding author   Language:English   Publishing type:Research paper (international conference proceedings)  

    DOI: 10.4230/LIPIcs.ECOOP.2020.9

  10. A Reversible Runtime Environment for Parallel Programs Reviewed

    Takashi Ikeda, Shoji Yuen

    Reversible Computation 2020, Lecture Notes in Computer Science   Vol. 12247   page: 272-279   2020.7

     More details

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

    DOI: 10.1007/978-3-030-52482-1_18

  11. Fault Diagnosis for Distributed Cooperative System Using Inducting Logic Programming Invited Reviewed

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

    IEEE International Conference on Prognostics and Health Management, ICPHM 2020     page: 1 - 8   2020.6

     More details

    Authorship:Corresponding author  

    DOI: 10.1109/ICPHM49022.2020.9187032

  12. Automating Time-series Safety Analysis for Automotive Control Systems Using Weighted Partial Max-SMT Reviewed

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

    Journal of Information Processing   Vol. 28   page: 124-135   2020.1

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

    DOI: 10.2197/ipsjjip.28.124

  13. Session-ocaml: A session-based library with polarities and lenses Reviewed

    Keigo Imai, Nobuko Yoshida, Shoji Yuen

    Science of Computer Program   Vol. 172   page: 135-159   2019.3

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

    DOI: 10.1016/j.scico.2018.08.005

  14. Reversing Event Structure Reviewed

    Irek Ulidowski, Iain Phillips, Shoji Yuen

    New Generation Computing   Vol. 36   page: 281-306   2018.9

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

    DOI: 10.1007/s00354-018-0040-8

  15. Reversing Parallel Programs with Blocks and Procedures Reviewed

    James Hoey, Irek Ulidowski, Shoji Yuen

    EPTCS (EXPRESS/SOS 2018)   Vol. 276   page: 69-86   2018.9

     More details

    Language:English  

    DOI: 10.4204/EPTCS.276.7

  16. Nested Timed Automata with Invariants Reviewed

    Yuwei Wang, Guoqiang Li, Shoji Yuen

    Lecture Notes in Computer Science   Vol. 10606   page: 77-93   2017.10

     More details

    Language:English  

    DOI: 10.1007/978-3-319-69483-2

  17. Nested Timed Automata with Diagonal Constraints Reviewed

    Yuwei Wang, Yunqing Wen, Guoqiang Li, Shoji Yuen

    Lecture notes in computer science   Vol. 10610   page: 396-412   2017.11

     More details

    Language:English  

    DOI: 10.1007/978-3-319-68690-5_24

  18. Reversing Imperative Parallel Programs. Reviewed

    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

     More details

    Language:English  

    DOI: 10.4204/EPTCS.255.4

  19. Session-ocaml: A Session-Based Library with Polarities and Lenses Reviewed

    Keigo Imai, Nobuko Yoshida, Shoji Yuen

    Lecture Notes in Computer Science   Vol. 10319   page: 99-118   2017.6

     More details

    Language:English  

    DOI: 10.1007/978-3-319-59746-1_6

  20. Automating Time Series Safety Analysis for Automotive Control Systems in STPA Using Weighted Partial Max-SMT Reviewed

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

    Communications in Computer and Information Science   ( 694 ) page: 39-54   2016.11

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

    DOI: 10.1007/978-3-319-53946-1_3

  21. An Over-Approximation Forward Analysis for Nested Timed Automata Reviewed

    Yunqing Wen, Guoqiang Li, Shoji Yuen

    Lecture Notes in Computer Science   Vol. 8979   page: 1-15   2015.1

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

  22. Nested Timed Automata with Frozen Clocks Reviewed

    Guoqiang Li, Mizuhito Ogawa, Shoji Yuen

    Lecture Notes in Computer Science   Vol. 9268   page: 189-205   2015.9

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

    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.

  23. Concurrency and reversibility Invited Reviewed

    Irek Ulidowski, Iain Phillips and Shoji Yuen

    Reversible Computation 2014, LNCS 8507   ( 8507 ) page: 1-14   2014.7

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

  24. 値付きタスクオートマトンに基づくコストを意識した実時間タスクスケジューリング

    結縁祥冶、亀井達朗

    信学技報   Vol. 114 ( 127 ) page: 37-42   2014.7

     More details

    Authorship:Lead author   Language:Japanese   Publishing type:Research paper (scientific journal)  

  25. 離散事象システムにおけるMaxSATソルバを用いた最大可制御部分仕様の導出

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

    信学技報   Vol. 114 ( 271 ) page: 35-40   2014.10

     More details

    Language:Japanese   Publishing type:Research paper (scientific journal)  

  26. 部分観測におけるMaxSATソルバを用いたスーパバイザ合成手法

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

    信学技報   Vol. 114 ( 416 ) page: 79-84   2015.1

     More details

    Language:Japanese   Publishing type:Research paper (scientific journal)  

  27. Modelling of Bonding with Process and Events Reviewed

    Iain Phillips, Irek Ulidowski, Shoji Yuen

    Lecture Notes in Computer Science   Vol. 7948   page: 141-154   2013.7

     More details

    Language:English  

  28. Modelling and analysis of real-time systems with mutex components Reviewed

    Guoqiang Li, Xiaojuan Cai, Shoji Yuen

    International Journal of Foundations of Computer Science   Vol. 25 ( 4 ) page: 831-851   2012.6

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

    DOI: 10.1142/S0129054112400382

  29. A Reversible Process Calculus and the Modelling of the ERK signalling pathway Reviewed

    Iain Phillips, Irek Ulidowski and Shoji Yuen

    In Proceedings of the 4th workshop on reversible computation RC2012     page: 227-239   2012.7

     More details

    Language:English  

  30. A session type systems with subject reduction Reviewed

    Keigo Imai, Shoji Yuen, and Kiyoshi Agusa

    IEICE Transaction, Infromatoin adn systems   Vol. E95-D ( 8 ) page: 2053--2064   2012.8

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

  31. タスクマイグレーション機能を持つマルチコアスケジューリング解析

    中堂園貴幸,結縁祥治

    信学技法   Vol. 112 ( 458 ) page: 103-108   2013.3

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

  32. 名前渡しプロセス計算における優先度ガード Reviewed

    結縁祥治, 太田正悟

    プログラミングおよびプログラミング言語ワークショップ     page: 246-257   2011.3

     More details

    Authorship:Lead author   Language:Japanese  

  33. Modeling and Analysis of Real -Time Systems with Mutex Components Reviewed

    Guoqiang Li, Xiaojuan Cai, Shoji Yuen

    Advances in Parallel and Distributed Computing Models   ( 3 ) page: 1-8   2010.4

     More details

    Language:English  

  34. Session Type Inference in Haskell Reviewed

    Keigo Imai, Shoji Yuen, Kiyoshi Agusa

    PLACES '10: Programming Language Approaches to Concurrency and Communication-cEntric Software     page: 43-52   2010.3

     More details

    Language:English  

  35. Communication Centered Dependable GUI Programmingbased on Choreography

    Sho SHIMOMURA and Shoji YUEN

    IEICE Technical Report (Software Science)   Vol. 109 ( 456 ) page: 127-132   2010.3

     More details

    Language:Japanese  

  36. A Type-Based Analysis for Checking Race and Deadlockbased on Access Capabilities

    Yoshitaka BANNO and Shoji YUEN

    IEICE Technical Report (Software Science)   Vol. 109 ( 456 ) page: 133-138   2010.3

     More details

    Language:Japanese  

  37. 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

     More details

    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.

  38. 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

     More details

    Language:Japanese  

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

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

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

     More details

    Authorship:Lead author   Language:Japanese  

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

    Li Guoqiang, Shoji Yuen, and Masakazu Adachi

        page: 133-147   2009.3

     More details

    Language:English  

  41. A full implementation of session types in Haskell Reviewed

    Keigo Imai, Shoji Yuen, and Kiyoshi Agusa

        page: 44-56   2009.3

     More details

    Language:English  

  42. Energy Efficient Functional Programing on DVS Systemsby Varying Evaluation Strategies Reviewed

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

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

     More details

    Language:Japanese   Publishing type:Research paper (scientific journal)  

  43. *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

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

  44. 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

     More details

    Language:Japanese  

  45. Dependable software design based on communication centered programming

    Shoji Yuen

    DSW2008     page: 135   2008.7

     More details

    Authorship:Lead author   Language:Japanese  

  46. Communicating Processes with Timed Behavioral Extension Invited Reviewed

    Shoji Yuen

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

     More details

    Authorship:Lead author   Language:Japanese  

  47. 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

     More details

    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.

  48. 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

     More details

    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.

  49. A Deadlock free analysis for AIBO OPEN-R programs based on communicating processes Reviewed

    Ryo Suetsugu, Shoji Yuen, Kiyoshi Agusa

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

     More details

    Language:Japanese   Publishing type:Research paper (scientific journal)  

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

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

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

     More details

    Language:Japanese  

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

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

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

     More details

    Language:Japanese  

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

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

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

     More details

    Language:Japanese  

  53. 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

     More details

    Language:Japanese   Publishing type:Research paper (scientific journal)  

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

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

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

     More details

    Language:Japanese   Publishing type:Research paper (scientific journal)  

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

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

     More details

    Authorship:Lead author   Language:Japanese  

  56. *Web Automata: A Behavioral Model of Web Applications based on the MVC Reviewed

    Shoji Yuen, Keishi Kato, Daiju Kato, Kiyoshi Agusa

    Computer Software   Vol. 22   page: 44-57   2005

     More details

    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.

  57. Name-passing style GUI Programming in a pi-calculus-based language Nepi Reviewed

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

    Electric Notes of Theoretical Computer Science   Vol. 139   page: 145-168   2005

     More details

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

    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.

  58. Towards Assurign Quality Attributes of Client Dynamic Web Applications: Identifying and Addressing the Challenges Reviewed

    Mohammed Sharaf Aun, Shoji Yuen, Kiyoshi Agusa

    Journal of Web Engineering   Vol. 4   page: 144-164   2005

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

  59. 通信プロセスモデルに基づく並行オブジェクト指向言語によるAIBOプログラムの動作記述 Reviewed

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

    ソフトウェア工学の基礎ワークショップFOSE2005     page: 267-276   2005.11

     More details

    Language:Japanese  

  60. *Process languages with discrete relative time based on the Ordered SOS format and rooted eager bisimulation Reviewed

    Irek Ulidowski, Shoji Yuen

    The Journal of Logic and Algebraic Programming   Vol. 60-61   page: 401-460   2004.12

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

    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.

  61. Name-passing style GUI programming in the π-calculus-based language Nepi Reviewed

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

     More details

    Authorship:Lead author   Language:English  

  62. An Approach for Debugging Client Dynamic Web Applications Reviewed

    Mohammed Sharaf Aun, Shoji Yuen, Kiyoshi Agusa

      Vol. 45   page: 2373-2383   2004

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

  63. FCDG に基づいたコーディングパターン Reviewed

    コンピュータソフトウェア   Vol. 21 ( 4 ) page: 27-36   2004

     More details

    Language:Japanese   Publishing type:Research paper (scientific journal)  

  64. 時間付きπ計算によるリアルタイムオブジェクト指向言語の形式的記述 Reviewed

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

    情報処理学会論文誌   Vol. 45 ( 6 ) page: 1498-1507   2004

     More details

    Language:Japanese   Publishing type:Research paper (scientific journal)  

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

  65. π計算に対する時間拡張と代数的意味論 Reviewed

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

    ソフトウェア工学の基礎ワークショップFOSE2004     page: 97-108   2004.11

     More details

    Language:Japanese  

  66. 時間オートマトンの遷移制約記述に基づくAIBOプログラムスケルトンコードの生成手法 Reviewed

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

    組込みソフトウェアシンポジウム2004     page: 126-133   2004.10

     More details

    Language:Japanese  

  67. Testing Framework for Web Applications based on the MVC model with Behavioral Description Reviewed

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

    Proceedings of ICITA     page: 11-4:1-6   2004.1

     More details

    Authorship:Lead author   Language:English  

  68. 実行可能なメモリモデルに基づくJava並行プログラムのモデル検査 Reviewed

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

    ソフトウェア工学の基礎ワークショップFOSE2003     page: 227-238   2003.11

     More details

    Language:Japanese  

  69. 時間つきπ計算によるリアルタイムオブジェクト指向言語の形式的記述 Reviewed

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

    オブジェクト指向最前線     page: 69-76   2003.8

     More details

    Language:Japanese  

  70. Process Languages for Rooted Weak Preorders

    Irek Ulidowski, Shoji Yuen

    Technical Report , University of Leicester   Vol. 2002 ( 11 )   2002

     More details

    Language:English   Publishing type:Research paper (bulletin of university, research institution)  

  71. A Semi-Multihoming Technique Using Network Address Translator Reviewed

    Shoji Kajita, Shoji Yuen

    Journal of Information Processing Society of Japan   Vol. 42 ( 12 )   2001

     More details

    Language:Japanese   Publishing type:Research paper (scientific journal)  

    This paper presents a multihoming technique for a middle or small sized network using NAT (Network Address Translator). We call our technique semi-multihoming since we only consider the user-side multihoming, where the typical multihoming enables to bridge the cdonnections while ours does not. THe advantage of our technique is that the flexible load-balancing between the connections is possible based on the local routing policy independent of the global policy to which the network may belong. NAT is the key technology to enable our technique to implement on the existing network equipments. FInally, we show an impementation and the result of our technique at Center for Information Media Studies, Nagoya University.

  72. Timed Properties for Process Languages with Time Reviewed

    Irek Ulidowski and Shoji Yuen

    In Proceedings of SCI2001, Volume XIV     page: 344-349   2001

     More details

    Authorship:Lead author   Language:English  

    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.

  73. General Process Languages with Time

    Irek Ulidowski, Shoji Yuen

    Technical Report, University of Leicester   Vol. 2000 ( 41 )   2000

     More details

    Language:English   Publishing type:Research paper (bulletin of university, research institution)  

  74. Process Languages for Rooted Eager Bisimulation Reviewed

    Lecture Notes in Computer Science   Vol. 1877   page: 275,289   2000.8

     More details

    Language:English  

  75. *Testing Theory for Probabilistic Processes Reviewed

    Rance Cleaveland, Zeynep Dayar, Scott Smolka, Shoji Yuen

    Information and Computation   Vol. 154   page: 93-148   1999

     More details

    Language:English   Publishing type:Research paper (scientific journal)  

  76. Symbolic Alternative Characterizations of Testing Preorders for Rugular Real-time Communicating Processes

      Vol. J80-D-1 ( 6 ) page: 474-485   1997

     More details

    Authorship:Lead author   Language:Japanese   Publishing type:Research paper (scientific journal)  

  77. Extending Process Language with Time Reviewed

    Lecture Notes In Computer Science   Vol. 1349   1997

     More details

    Authorship:Lead author   Language:English  

  78. Fully Abstract Characterizations of Testing Preorders for Probabilistic Processes Reviewed

    Lecture Notes in Computer Science   Vol. 836   page: 497-512   1994

     More details

    Authorship:Lead author   Language:English  

  79. An extension of the testing method for processes passing infinite values Reviewed

    Shoji Yuen, Toshiki Sakabe, Yasuyoshi Inagaki

    Workshop in Computing     page: 155-173   1993

     More details

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

  80. An Extension of the Testing Method for Processes Passing Infinite Values Reviewed

    The John Hopkins University     page: 10:1-20   1992.8

     More details

    Authorship:Lead author   Language:English  

  81. CCSによるモニタ記述の形式的記述 Reviewed

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

    電子情報通信学会論文誌   Vol. J73-D-1   page: 683-692   1990

     More details

    Authorship:Lead author   Language:Japanese   Publishing type:Research paper (scientific journal)  

▼display all

Books 2

  1. 理論計算機科学事典 Reviewed

    結縁祥治( Role: Contributor ,  6.4 並行計算)

    朝倉書店  2022.1 

     More details

    Total pages:807   Responsible for pages:586-603   Language:Chinese Book type:Dictionary, encyclopedia

  2. 並行プロセスの操作的および代数的意味論

    稲垣康義、結縁祥治( Role: Joint author)

    丸善  1993 

     More details

    Language:Japanese

Presentations 9

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

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

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

     More details

    Event date: 2024.3

    Language:Japanese   Presentation type:Oral presentation (general)  

    Venue:石垣市健康福祉センター   Country:Japan  

  2. Bidirectional Flow analysis for a concurrent reversible programming language

    Shoji Yuen

    2024.2.28 

     More details

    Event date: 2024.2

    Language:English   Presentation type:Public lecture, seminar, tutorial, course, or other speech  

    Venue:University of Urbino, Italy   Country: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.

    Other Link: https://www.uniurb.it/novita-ed-eventi/5685

  3. Constant Propagation in CRIL by Bidirectional Data Flow Analysis

    Shunya Oguchi and Shoji Yuen

    2024.1.11 

     More details

    Event date: 2024.1

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

    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.

  4. 充足可能性判定を利用した実現可能な時間オートマトンの検証

    城 聖一郎,結縁祥治

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

     More details

    Event date: 2022.7

    Language:Japanese   Presentation type:Oral presentation (general)  

    Venue:札幌市   Country:Japan  

  5. 通信プロセスに対する文脈変換手法を用いたモデル検査

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

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

     More details

    Event date: 1999

    Language:Japanese   Presentation type:Oral presentation (general)  

    Country:Japan  

    電子情報通信学会技術報告COMP98-82, pp.25-32

  6. 時間オートマトンによる振舞いモデルに基づく高信頼Real-time Javaコード生成手法

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

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

     More details

    Event date: 2005.3

    Language:Japanese   Presentation type:Oral presentation (general)  

    Country:Japan  

  7. Communication Centered Programming of Integrated Services with Priority in Home Appliance Network International conference

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

     More details

    Event date: 2009.10

    Language:English   Presentation type:Oral presentation (general)  

    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

  8. Session types in OCaml International conference

    Keigo Imai, Nobuko Yoshida, Shoji Yuen

    Theory and Applications of Behavioural Types (Dagstuhl Seminar 17051) 

     More details

    Event date: 2017.1 - 2017.2

    Language:English   Presentation type:Oral presentation (general)  

    Country:Germany  

  9. タスクマイグレーション機能を持つマルチコアスケジューリング解析

    中堂園貴幸, 結縁祥治

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

     More details

    Event date: 2013.3

    Language:Japanese   Presentation type:Oral presentation (general)  

    Country:Japan  

▼display all

Research Project for Joint Research, Competitive Funding, etc. 4

  1. Mathematical structures for software verification based on practical efficient behavior

    2015.3 - 2017.12

      More details

    Grant type:Competitive

  2. 高信頼車載システムの検証手法の研究

    2007.4 - 2009.3

    国内共同研究 

      More details

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

  3. Webアプリケーション指向ソフトウェアモデリング

    2002.11 - 2006.3

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

      More details

    Grant type:Competitive

    Webアプリケーションの意味論の基礎を成す形式体系、さらに、これらに基づいて提案されている言語、形式モデルとは独立に提案されている言語などを検討し、新たな計算モデルの形式化を行う。

  4. A Behavioral Analysis of Real-time Concurrent Software based on Sturactural Operational Semantics

    2001 - 2002

      More details

    Grant type:Competitive

KAKENHI (Grants-in-Aid for Scientific Research) 2

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

    2007

    科学研究費補助金  基盤研究(C)(一般),課題番号:19500026

    結縁 祥治

      More details

    Authorship:Principal investigator 

  2. データと時間を扱うオートマトンネットワークの合成的アクティブ学習に基づく設計手法

    Grant number:21H03415  2021.4 - 2026.3

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

      More details

    Authorship:Principal investigator  Grant type:Competitive

    Grant amount:\17030000 ( Direct Cost: \13100000 、 Indirect Cost:\3930000 )

Industrial property rights 1

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

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

     More details

    Applicant:日本電信電話株式会社

    Application no:特願2004-165578  Date applied:2004.6

    Country of applicant:Domestic  

 

Teaching Experience (On-campus) 4

  1. First Year Seminar A

    2011

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

    2001

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

    2001

  4. 計算機基礎数理

    2000

Teaching Experience (Off-campus) 1

  1. 情報工学概論

    2006.4 - 2007.3 名城大学)