| IEICE Technical Committee Submission System Conference Schedule |
Online Proceedings [Sign in] Tech. Rep. Archives |
All Technical Committee Conferences (Searched in: All Years)
| Committee | Date Time | Place | Paper Title / Authors | Abstract | Paper # | |
| SS | 2024-03-07 13:30 |
Okinawa | (Primary: On-site, Secondary: Online) |
Zone-Based Reachability Analysis of Nested Timed Automata Seiichiro Tachi (Nagoya Univ), Mizuhito Ogawa (JAIST), Shoji Yuen (Nagoya Univ)  SS2023-53 |
We present a zone-based reachability analysis for Nested Timed Automata (NeTA). NeTA is a timed pushdown automaton that... [more] |
SS2023-53 pp.25-30 |
| SS, IPSJ-SE, KBSE [detail] | 2022-07-29 13:00 |
Hokkaido | Hokkaido-Jichiro-Kaikan (Sapporo) (Primary: On-site, Secondary: Online) |
Verification of Implementable Timed Automata via Satisfiability Checking Seiichiro Tachi, Shoji Yuen (Nagoya Univ.) SS2022-9 KBSE2022-19 |
We present a technique for bounded model-checking the reachability in timed automata with implementability assuming that... [more] | SS2022-9 KBSE2022-19 pp.49-54 |
| SS | 2022-03-07 14:30 |
Online | Online | Learning Assumptions for Compositional Verification of Timed Systems with Tree Queries Kotaro Niimi, Shoji Yuen (Nagoya Univ) SS2021-49 |
This paper presents an automatic assumption-learning for compositional verification of timed systems. We focus on Assume... [more] | SS2021-49 pp.43-48 |
| DC, SS | 2019-10-24 14:30 |
Kumamoto | Kumamoto Univ. | Computing Optimal Weight in Weighted Register Automata and Related Decision Problems Reo Yoshimura (Nagoya Univ.), Yoshiaki Takata (Kochi-tech.), Hiroyuki Seki (Nagoya Univ.) SS2019-16 DC2019-44 |
Register automaton (RA) is a computational model that can handle data values by adding registers to finite automaton. Re... [more] | SS2019-16 DC2019-44 pp.19-24 |
| SS | 2018-03-06 11:30 |
Okinawa | Model Checking Application to the Railway Crossing Problem for STAMP/STPA using Timed Automaton Kozo Okano, Shinpei Ogata, Pan Yang (Shinshu Univ.), Keishi Okamoto (Sendai National College of Tech.) SS2017-64 |
Recent rapid growth of information systems makes us pay attention to methods for analysis of accident causation and pr... [more] |
SS2017-64 pp.1-6 |
|
| SS | 2017-03-09 09:30 |
Okinawa | A Symbolic Simulation of Dense-Timed Pushdown Automata with Clock Freezing Sho Hiraoka, Shoji Yuen (Nagoya Univ.) SS2016-60 |
We present a symbolic simulation based on a zone construction for the dense timed pushdown automata with clock freezing(... [more] | SS2016-60 pp.1-6 |
|
| DC, SS | 2016-10-27 15:05 |
Shiga | Hikone Kinro-Fukushi Kaikan Bldg. | Towards a Zone-based Verification for DTPDA with Clock Freezing Sho Hiraoka, Shoji Yuen (Nagoya Univ.) SS2016-25 DC2016-27 |
We present a zone construction for the dense timed pushdown automata with freezing ages as a discretization method to ve... [more] | SS2016-25 DC2016-27 pp.43-48 |
| SS | 2015-05-11 13:50 |
Kumamoto | Kumamoto University | An Implementation of Computing Optimal Mean-payoff Values for Non-terminating Scheduling by Double Priced Timed Automata Sho Hiraoka, Shoji Yuen (Nagoya Univ.) SS2015-3 |
Derivation of the optimal behavior for scheduling such as Operating System using double priced timed automata, DPTA for ... [more] | SS2015-3 pp.11-16 |
| SS | 2014-10-23 15:45 |
Kochi | Kochi city culture-plaza cul-port | Code synthesis for LEGO Mindstorms EV3 using UPPAAL Mitsuru Arakawa, Shoji Yuen (Nagoya Univ.) SS2014-32 |
We present a code synthesis for controlling the LEGO Mindstorm EV3 using UPPAAL as the designing tool. UPPAAL is a model... [more] | SS2014-32 pp.41-46 |
| SWIM | 2014-08-21 14:35 |
Kyoto | Ryukoku Univ.Ouniya Canvas | Validation of UML Timing Diagrams Using Timed Automata Kengo Kajimura, Yoshiyuki Shinkawa (Ryukoku Univ.) SWIM2014-11 |
Originally, UML had mainly been widely used as a model description language for analyzing, designing, manufacturing and ... [more] | SWIM2014-11 pp.17-21 |
| KBSE, SS, IPSJ-SE [detail] | 2014-07-10 10:00 |
Hokkaido | Furano-Bunka-Kaikan | A cost-aware scheduling for real-time tasks based on the priced task automta Shoji Yuen, Tatsuro Kamei (Nagoya Univ.) SS2014-11 KBSE2014-14 |
This report presents a technique to give the optimal cost with respect to time passage when a set of tasks are schedul... [more] |
SS2014-11 KBSE2014-14 pp.37-42 |
| SWIM | 2010-06-04 16:30 |
Tokyo | Kikai-Shinko-Kaikan Bldg. | Validity Checking for UML Models Containing Time Constraints Masato Nomura, Yoshiyuki Shinkawa (Ryukoku Univ.) SWIM2010-7 |
This paper discusses a validation process for UML sequence diagrams using a model checking tool UPPAAL. Since UPPAAL dea... [more] | SWIM2010-7 pp.45-50 |
| VLD | 2009-03-12 15:15 |
Okinawa | Formal verification of GALS system designs using UPPAAL Kazuaki Kirita, Tomoyuki Yokogawa, Hisashi Miyazaki, Yoichiro Sato, Michiyoshi Hayase (Okayama Pref. Univ.) VLD2008-150 |
To design GALS (Globally Asynchronous Locally Synchronous) systems, it is necessary to verify the correctness of behavi... [more] |
VLD2008-150 pp.141-146 |
|
| SS | 2009-03-02 17:00 |
Saga | Saga University | [Invited Talk]
Model Checking of Timed Automata Akio Nakata (Hiroshima City Univ.) SS2008-53 |
In this paper, we briefly describe model checking of timed automata, one of the verification techniques of real-time sys... [more] | SS2008-53 pp.29-34 |
| CAS, MSS | 2008-11-06 16:15 |
Osaka | Osaka University | Predicate Abstraction and Refinement of Parallel Behaviour of Hierarchical Timed Automata Shinichi Yamazaki, Satoshi Yamane, Masatoshi Yasui (Kanazawa Univ.) CAS2008-50 CST2008-28 |
In this paper, we propose the predicate abstraction and refinement verification method for the paralell hierarchical tim... [more] | CAS2008-50 CST2008-28 pp.31-36 |
| SS | 2008-03-04 11:25 |
Nagasaki | Nagasaki Univ. | Abstraction of Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop Takeshi Nagaoka, Kozo Okano, Shinji Kusumoto (Osaka Univ.) SS2007-74 |
We have proposed a method of model abstraction for timed automata.The proposed method is based on CEGAR (CounterExample... [more] | SS2007-74 pp.103-108 |
| MSS | 2007-08-31 14:45 |
Shimane | Shimane University | Design Verification Technique of A Soft Real-Time System using UML and Utility Function Satoshi Yamane, Masaaki Sakakura (Kanazawa Univ.) CST2007-15 |
Recently, in the real-time systems used in many scenes, soft real-time systems, which are not strict by the deadline, ... [more] |
CST2007-15 pp.25-30 |
| SS | 2007-08-03 11:45 |
Hokkaido | Hokkaido Univ. | Abstraction of Extended Timed Automata for UPPAAL Based on Counterexample-Guided Abstraction Refinement Loop Takeshi Nagaoka, Kozo Okano, Shinji Kusumoto (Osaka Univ) SS2007-29 |
In the model checking of the realtime systems, the number of states of models increases exponentlly with the number of t... [more] | SS2007-29 pp.77-82 |
| COMP | 2007-04-26 14:25 |
Kyoto | Katsura Campus, Kyoto University | Implementation of Probabilistic Timed Strong Simulation Algorithm Yuki Hasizume, Satoshi Yamane (Kanazawa Univ.) COMP2007-6 |
It is useful for real-time systems with probabilistic behaviors to verify formally probabilistic timed automata. Probabi... [more] | COMP2007-6 pp.41-48 |
| MSS | 2006-07-26 13:25 |
Kyoto | Kyoto Institute of Technology | Development of strong probabilistic timed simulation verifier of probabilistic timed automata Satoshi Yamane, Hiroshi Kodera, Tsuneo Arai (Kanazawa Univ.) |
In 2003, we have shown the decidability of the problem：「On the "Probabilistic Timed Automata", Strong Probabilistic Ti... [more] |
CST2006-15 pp.31-35 |
[Return to Top Page]