| 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 # | |
| KBSE | 2024-03-15 13:20 |
Okinawa | Okinawa Prefectual General Welfare Center (Primary: On-site, Secondary: Online) |
On Improvement of Variability Model Division Method Tomoji Kishi (Waseda Univ.)  KBSE2023-87 |
The analysis and verification of variability models are often based on logic, but the number of configurations of a vari... [more] | KBSE2023-87 pp.120-125 |
| KBSE, SC | 2023-11-17 15:30 |
Miyagi | Sento Kaikan | Variability Model Division for Scalability Improvement Tomoji Kishi (WU) KBSE2023-37 SC2023-20 |
Variability models have been used for logic-based analysis and verification, but the number of variations is combinatori... [more] | KBSE2023-37 SC2023-20 pp.31-36 |
| KBSE | 2023-03-16 15:10 |
Hiroshima | JMS ASTERPLAZA (Primary: On-site, Secondary: Online) |
Traceability Management Method based on Informal/Semi-formal Hybrid Notation Ryoji Okada, Yoshihiro Ohama, Seigo Ito (TCRDL) KBSE2022-56 |
For traceability management of design specification in software and system designing, methods using informal notation, o... [more] | KBSE2022-56 pp.13-18 |
| MSS, CAS, IPSJ-AL [detail] | 2018-11-13 15:15 |
Shizuoka | On formal verification of mathematical programming models by algebraic specifications Masaki Nakamura, Kazutoshi Sakakibara (Toyama Pref. Univ.) CAS2018-76 MSS2018-52 |
To apply a solver for optimization problems, we need to formalize a problem into a form acceptable by the solver. In th... [more] |
CAS2018-76 MSS2018-52 pp.127-130 |
|
| SS, KBSE, IPSJ-SE [detail] | 2017-07-19 10:45 |
Hokkaido | Deadlock Detection in Scheduling of Last-Mile Transportation by Using Model Checking Mitsuaki Tsuji, Koji Hasebe, Kazuhiko Kato (Univ. of Tsukuba) SS2017-2 KBSE2017-2 |
The authors are developing a last-mile transportation system with autonomous vehicles. The greatest feature is that pass... [more] | SS2017-2 KBSE2017-2 pp.7-12 |
|
| SS | 2015-03-09 09:55 |
Okinawa | OKINAWAKEN SEINENKAIKAN | Reactive System Synthesis with Tolerance for Unexpected Environmental Behavior Atsushi Ueno, Takashi Tomita, Masaya Shimakawa, Shigeki Hagihara, Naoki Yonezaki (Tokyo Tech) SS2014-56 |
On the synthesis of reactive system (RS), if we assume some behavior property on an environment, specifications must inc... [more] | SS2014-56 pp.7-12 |
| VLD, DC, IPSJ-SLDM, CPSY, RECONF, ICD, CPM (Joint) [detail] |
2014-11-26 10:45 |
Oita | B-ConPlaza | A hardware description method and sematics providing a timing constrant Shunji Nishimura, Motoki Amagasaki, Toshinori Sueyoshi (Kumamoto Univ.) VLD2014-82 DC2014-36 |
Formal verification methods are wide-spreading due to its mathmatical rigorousaspect, although they limited to synchroun... [more] | VLD2014-82 DC2014-36 pp.81-86 |
| RECONF | 2014-09-19 14:40 |
Hiroshima | Formal Verification System of Multi-clock Synchronous Circuits on Multimodal Logic Shunji Nishimura, Motoki Amagasaki, Toshinori Sueyoshi (Kumamoto Univ.) RECONF2014-33 |
Regardless of wide using of a formal verification methods, almost all of the methods limited to single-clock synchrounou... [more] | RECONF2014-33 pp.93-98 |
|
| SC, IPSJ-UBI | 2014-07-28 10:00 |
Tokyo | National Institute of Informatics | Formal verification for service composition of formaly verified services using different mechanisms Kazuhiro Funakoshi, Shigeru Hosono (NEC) SC2014-6 |
This presentation describes a case study to generate models on proof assistant Coq with input of multiple Web services' ... [more] | SC2014-6 pp.49-54 |
| SS | 2014-03-11 10:30 |
Okinawa | Tenbusu Naha | Generation and Verification of Decision Table using SAT Solver Shinji Itoh, Naoto Sato, Hidetaka Kondoh, Kunihiko Miyazaki, Hiroki Mori, Makoto Kimura, Kiyoshi Yamaguchi (Hitachi) SS2013-73 |
Use of a decision table is an effective method to prevent defects of combination patterns of conditions. However, it is ... [more] | SS2013-73 pp.7-11 |
| IN, NV (Joint) |
2013-07-19 15:15 |
Hokkaido | Hokkaido Univ. Faculty of Eng. Academic Lounge 3 | Model Checking of OpenFlow Network with Abstraction of Packets Based on Symbolic Execution Yutaka Yakuwa, Nobuyuki Tomizawa, Toshio Tonouchi (NEC) IN2013-54 |
We propose a verification method of the OpenFlow network with the model checking, which can detect a loop routing and so... [more] | IN2013-54 pp.107-112 |
| KBSE | 2013-03-14 15:30 |
Tokyo | Shibaura Institute of Technology | Model checking potential deadlocks of DB transactions Takuya Saruwatari, Hideaki Tsukamoto, Shingo Kamiya, Shunsuke Miyata (NTT) KBSE2012-76 |
Improvement of IT system’s dependability using formal methods is expected. In a typical IT system development, formal me... [more] | KBSE2012-76 pp.43-48 |
| KBSE | 2013-03-15 11:25 |
Tokyo | Shibaura Institute of Technology | A proposal on architecture based verification case Shuichiro Yamamoto (Nagoya Univ.) KBSE2012-82 |
Although formal method is attracted to verify system correctness, it is not practical to verify every property of system... [more] | KBSE2012-82 pp.79-83 |
| DC | 2012-12-14 17:00 |
Fukui | Aossa (Fukui) | Verification of Automatic Block System for Single Line Using SMT Solver Natsuki Terada (RTRI) DC2012-79 |
Formal methods are expected to increase reliability of software, including that of signaling systems. We modeled the sp... [more] | DC2012-79 pp.31-36 |
| SWIM | 2012-11-30 11:00 |
Tokyo | Tokai Univ. Takanawa Campus(Tokyo) | Event-B Based Development for Mobile Applications Hitoshi Koshika, Yoshiyuki Shinkawa (Ryukoku Univ.) SWIM2012-16 |
The recent increasing complexity of software limits the improvement of its reliability and productivity through the trad... [more] | SWIM2012-16 pp.7-12 |
| SS | 2012-03-13 13:05 |
Okinawa | Tenbusu-Naha | A development assistance method for Ruby on Rails Application with Alloy Hiroaki Mizutani, Shoji Yuen (Nagoya Univ.) SS2011-64 |
We propose a development assistance method by converting Ruby on Rails Web application into Alloy models. Alloy analyzes... [more] | SS2011-64 pp.43-48 |
| DC | 2011-12-16 14:30 |
Hyogo | A Safety Estimation of the ATPB System using UML and Formal Method Guo Xie, Hiroshi Mochizuki, Sei Takahashi, Hideo Nakamura (Nihon Univ.) DC2011-70 |
This paper models and makes a formal analysis of the train control system of a novel railway system, ATPB system, which ... [more] | DC2011-70 pp.13-16 |
|
| SS | 2011-10-28 11:15 |
Ishikawa | JAIST | Iterative Construction of Finite Alloy Descriptions Kei Kogai (Ibaraki National College of Technology), Shin Nakajima (NII), Yoshikazu Ueda (Ibaraki Univ.) SS2011-36 |
In a process of creating Alloy descriptions, it is often to analyze the descriptions by scoped Alloy commands. The comma... [more] | SS2011-36 pp.55-60 |
| SWIM | 2011-06-17 16:25 |
Tokyo | Kikai-Shinko-Kaikan Bldg. | Implementation of the Event-B models using Haskell Hitoshi Koshika, Yoshiyuki Shinkawa (Ryukoku Univ.) SWIM2011-7 |
Formal methods in early development stages are recognized more effective for quality and productivity of software, in co... [more] | SWIM2011-7 pp.31-36 |
| SWIM | 2010-11-19 15:25 |
Tokyo | Tokai Univ. Takanawa Campus(Tokyo) | Verification of UML Sequence Diagrams with Time Constraints Yoshihiro Yasuda, Yoshiyuki Shinkawa (Ryukoku Univ.) SWIM2010-23 |
Verification of the system specification is usually performed independently from three major different viewpoints, that ... [more] | SWIM2010-23 pp.39-44 |
[Return to Top Page]