| 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 # | |
| MSS, NLP | 2022-03-28 10:05 |
Online | Online | Formal Verification of Control Policy of Elevator Systems using Statistical Model Checking Yuki Kitahara, Masaki Nakamura, Kazutoshi Sakakibara (Toyama Pref. Univ.)  MSS2021-57 NLP2021-128 |
When designing an elevator system, efficient control laws can be expected to be obtained by considering the probability ... [more] | MSS2021-57 NLP2021-128 pp.13-18 |
| SS | 2019-03-04 09:25 |
Okinawa | Behavioral Verification of Yampa Programs in a Discrete Runtime Environment using Uppaal Riku Nakane, Shoji Yuen (Nagoya Univ.) SS2018-52 |
This study proposes a verification of Yampa program behavior in the discrete runtime environment using Uppaal. Although ... [more] | SS2018-52 pp.1-6 |
|
| SWIM | 2015-12-05 14:50 |
Tokyo | Tokyo polytechnic Univ. | Performance Prediction for GAE Using the UPPAAL Sachi Nishida, Yoshiyuki Shinkawa (Ryukoku Univ.) SWIM2015-15 |
Recently, PaaS type cloud services like Google App Engine (GAE) are becoming a candidate for the system processing plat... [more] |
SWIM2015-15 pp.19-24 |
| KBSE | 2015-03-06 15:25 |
Tokyo | The University of Electro-Communications | Verifying Source Code with a Use Case Model using Model Checking
-- A Case of an ASP.NET Application -- Yoshitaka Aoki, Shinpei Ogata (Shinshu Univ.), Satoshi Yazawa (VR), Saeko Matsuura (SIT) KBSE2014-64 |
Model checking is an effective technique in order to verify the behavior of the system. We have proposed a method to fin... [more] | KBSE2014-64 pp.71-76 |
| 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 15:20 |
Hokkaido | Furano-Bunka-Kaikan | A Method of Facilitating Counterexample Analysis in Model Checking Yoshitaka Aoki (Nihon Unisys), Saeko Matsuura (Shibaura Inst. of Tech.) SS2014-16 KBSE2014-19 |
Model checking is an effective technique in order to verify the behavior of the system. We have proposed a method to fin... [more] | SS2014-16 KBSE2014-19 pp.87-92 |
| KBSE | 2014-05-30 13:45 |
Kanagawa | Keio Univ.(Raiou-sha, Hiyoshi Campus) | Dissemination and Use of Model Checking Tool in Enterprise Yoshitaka Aoki (Nihon Unisys), Saeko Matsuura (Shibaura Inst. of Tech.) KBSE2014-9 |
Model checking is a technique superior to inspect the behavior of the system. However, it is difficult writing the appr... [more] | KBSE2014-9 pp.47-52 |
| SS, KBSE | 2013-07-26 13:10 |
Hokkaido | Application to Development Site of Model Checking Technology
-- Discovery of Inconsistency of Specification and Source Code -- Yoshitaka Aoki (Nihon Unisys), Saeko Matsuura (Shibaura Inst. of Tech.) SS2013-28 KBSE2013-28 |
Software programs often include many defects that are not easy to detect because of the developers’ mistakes, misunderst... [more] | SS2013-28 KBSE2013-28 pp.91-96 |
|
| KBSE | 2013-03-14 10:05 |
Tokyo | Shibaura Institute of Technology | Verification of Program Defects Based on Model Checking Techniques for Development
-- Stable Checking with Inspection Support Tool -- Yoshitaka Aoki (Nihon Unisys), Saeko Matsuura (Shibaura Inst. of Tech.) KBSE2012-69 |
In the development site, difficult defects of detecting occurs when Miss inadequate requirements definition and implem... [more] | KBSE2012-69 pp.1-6 |
| KBSE | 2012-11-23 15:05 |
Ishikawa | Kanazawa University | An Automatic Use of Model Checking Tool for Validating Data Lifecycle Shinpei Ogata (Shinshu Univ.), Satoshi Yazawa, Kazuhiko Nishimura (VR), Yoshitaka Aoki, Hirotaka Okuda, Saeko Matsuura (SIT) KBSE2012-56 |
Model checking techniques are a promised technique to detect errors in a specification efficiently and exhaustively. How... [more] | KBSE2012-56 pp.109-114 |
| KBSE, SS | 2011-07-30 11:15 |
Hokkaido | Hokkaido Information University | On Generating Realtime Programs with Runtime Checking
-- From Timed Automata to Realtime Programs on Non-Realtime Environments -- Ilankaikone Senthooran, Julian Prokay, Takuo Watanabe (Tokyo Inst. of Tech.) SS2011-25 KBSE2011-22 |
We propose a method of generating realtime programs from verified models. The primary goal of this work is to provide an... [more] | SS2011-25 KBSE2011-22 pp.75-80 |
| SWIM | 2010-06-04 16:05 |
Tokyo | Kikai-Shinko-Kaikan Bldg. | Verification of Inter-Model Consistency between UML Activity and Sequence Diagram Yuuichi Dounishi, Yoshiyuki Shinkawa (Ryukoku Univ) SWIM2010-6 |
UML diagrams can express software structure and behavior precisely, however, no explicit definitions on inter-diagram re... [more] | SWIM2010-6 pp.39-44 |
| 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 |
| SWIM | 2010-02-26 16:25 |
Tokyo | Kikai Sinkukaikan B3-2 | Description and Verification of Time Constrains in UML Sequence Diagrams Yoshihiro Yasuda, Yoshiyuki Shinkawa (Ryukoku Univ.) SWIM2009-24 |
In UML 2.0, it is possible to describe time constraints in sequence diagrams. However it seems difficult to validate or ... [more] | SWIM2009-24 pp.27-32 |
| SS | 2009-12-18 09:40 |
Kagawa | Kagawa Univ. | A behavioral model for debugging multicore real-time applications based on execution traces Hiroki Mizuno, Shoji Yuen (Nagoya Univ) SS2009-43 |
This paper proposes a technique to effectively identify defects of realtime applications running in the multicore envir... [more] |
SS2009-43 pp.49-54 |
| 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 | 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 |
[Return to Top Page]