| 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, 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 |
| 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, DC | 2021-10-19 15:25 |
Online | Online | A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Register Automata Akira Onishi, Ryoma Senda (Nagoya Univ.), Yoshiaki Takata (KUT), Hiroyuki Seki (Nagoya Univ.) SS2021-17 DC2021-22 |
Register automaton (abbreviated as RA) is an extension of finite automaton by adding registers storing data values. RA ... [more] |
SS2021-17 DC2021-22 pp.23-28 |
| ITS, IEE-ITS | 2021-03-15 15:05 |
Online | Online | Model Checking-Based Verification of Token-Based Traffic Control for Roundabouts Tatsuhiro Tsuchiya (Osaka Univ.), Satoshi Otsuka (Hitachi) ITS2020-43 |
This paper reports the results of model checking-based verification of a traffic control mechanism for roundabouts. This... [more] | ITS2020-43 pp.41-44 |
| SS | 2021-03-03 10:25 |
Online | Online | A Subclass of LTL with the Freeze Quantifier Translatable into Register Automata Akira Onishi, Ryoma Senda (Nagoya Univ.), Yoshiaki Takata (KUT), Hiroyuki Seki (Nagoya Univ.) SS2020-29 |
Register automaton (abbreviated as RA) is an extension of finite automaton by adding registers storing data values. RA ... [more] |
SS2020-29 pp.7-12 |
| SS | 2021-03-04 13:25 |
Online | Online | Generating Exhaustive Counterexample and Path Constraint with Software Analysis Workbench and Symbolic PathFinder Rin Karashima, Shinpei Ogata, Kozo Okano (Shinshu Univ.) SS2020-41 |
Software Analysis Workbench (SAW) generates models from JVM bytecode by symbolic execution. Users can perform model che... [more] |
SS2020-41 pp.78-83 |
| DC, SS | 2020-10-19 13:25 |
Online | Online | LTL Model Checking for Register Pushdown Systems Ryoma Senda (Nagoya Univ.), Yoshiaki Takata (KUT), Hiroyuki Seki (Nagoya Univ.) SS2020-6 DC2020-23 |
A pushdown system (PDS) is known as an abstract model of recursive programs. For PDS, model checking methods have been ... [more] |
SS2020-6 DC2020-23 pp.7-12 |
| KBSE | 2020-03-06 13:30 |
Okinawa | Tenbusu-Naha (Cancelled but technical report was issued) |
A Method to Analyze the Proximate States to Hazards Based-on State Transition System for Supporting Safety Analysis Yusuke Suzuki, Shinpei Ogata, Yutaro Ohike (Shinshu Univ.), Yoshitaka Aoki (Nihon Unisys), Hiroyuki Nakagawa (Osaka Univ.), Kazuki Kobayashi, Kozo Okano (Shinshu Univ.) KBSE2019-47 |
STAMP (System-Theoretic Accident Model and Processes）/STPA (System-Theoretic Process Analysis) supports system developer... [more] | KBSE2019-47 pp.7-12 |
| SS | 2020-03-05 12:05 |
Okinawa | (Cancelled but technical report was issued) |
An Approach of Deriving Hazard Transition Series by Cooperation of STAMP/STPA and Model Checking Pan Yang, Kozo Okano, Shinpei Ogata (Shinshu Univ.), Keishi Okamoto (Sendai National College of Tech.) SS2019-56 |
The demand for research on the hazard analysis of information systems and the construction of countermeasures have been ... [more] | SS2019-56 pp.93-98 |
| ICSS, IPSJ-SPT | 2020-03-03 11:00 |
Okinawa | Okinawa-Ken-Seinen-Kaikan (Cancelled but technical report was issued) |
Model checking RNNs with modal μ-calculus Tatsuhiro Aoshima, Toshinori Usui (NTT) ICSS2019-88 |
Machine learning models have been applied to many cyber-physical systems such as self-driving cars, robotics, and factor... [more] | ICSS2019-88 pp.119-124 |
| KBSE, SC | 2019-11-08 11:30 |
Nagano | Shinshu University | A Method to Analyze NuSMV Counterexamples for Defect Cause Analysis Yutaro Ohike, Shinpei Ogata (Shinshu Univ.), Yoshitaka Aoki (Nihon Unisys, Ltd.), Hiroyuki Nakagawa (Osaka Univ.), Kazuki Kobayashi, Kozo Okano (Shinshu Univ.) KBSE2019-24 SC2019-21 |
Many state variables that are defined in a model may appear as conditional expressions in one specification on model che... [more] | KBSE2019-24 SC2019-21 pp.7-12 |
| SWIM, KBSE | 2019-05-25 09:45 |
Tokyo | Kikai-Shinko-Kaikan Bldg. | A Proposal of FRAM Support Method using Probabilistic Model Checker Yoshitaka Aoki (NUL), Shinpei Ogata (Shinshu Univ) KBSE2019-8 SWIM2019-8 |
FRAM (Functional Resonance Analysis Method) is an analysis method to analyze and model a complex technical system. The F... [more] | KBSE2019-8 SWIM2019-8 pp.49-56 |
| NLP, MSS (Joint) |
2019-03-15 15:55 |
Fukui | Bunkyo Camp., Univ. of Fukui | A derivation of weighted transition system for Simulink models from simulation results Ryota Owaki (Nagoya Univ), Shoji Yuen (Nagooya Univ) MSS2018-95 |
We propose a method to generate a symbolic weighted transition system from a Simulink model description. Continuous va... [more] |
MSS2018-95 pp.75-80 |
| SS | 2019-03-04 10:15 |
Okinawa | Statistical model checking of hybrid systems with Acumen Kosuke Inoue, Daisuke Ishii (Fukui Univ.) SS2018-54 |
An integrated tool for modeling, simulation and verification is useful for developing reliable continuous/discrete hybri... [more] | SS2018-54 pp.13-18 |
|
| SS | 2019-03-05 15:25 |
Okinawa | Automatic Repair of Conditional Expressions for Functional Programs by Using Counterexamples Ken Matsui, Ryosuke Sato, Naoyasu Ubayashi, Yasutaka Kamei (Kyushu Univ.) SS2018-80 |
In software development, manual bug fixing consumes much time and effort. Therefore, automated program repair methods ha... [more] | SS2018-80 pp.169-174 |
|
| MSS, CAS, IPSJ-AL [detail] | 2018-11-13 14:50 |
Shizuoka | Process mining approach for the conformance checking of discrete-event simulation model Kenji Uehara, Kunihiko Hiraishi (JAIST) CAS2018-75 MSS2018-51 |
Discrete-event simulation is an effective method to reproduce the target system behavior and to investigate its mechanis... [more] | CAS2018-75 MSS2018-51 pp.121-126 |
|
| KBSE, SS, IPSJ-SE [detail] | 2018-07-18 15:50 |
Hokkaido | Case Study on a Verification of an IoT Architecture Model Based on Control Loop Yoshitaka Aoki (NUL), Shinpei Ogata, Kazuki Kobayashi (Shinshu Univ.), Hiroyuki Nakagawa (Osaka Univ.) SS2018-11 KBSE2018-21 |
IoT (Internet of Things) systems have their respective complicated configuration across cyber and physical space. Even i... [more] | SS2018-11 KBSE2018-21 pp.61-66 |
|
| 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, 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, KBSE, IPSJ-SE [detail] | 2017-07-19 13:10 |
Hokkaido | Prototyping and Evaluation of Support Method of Model Checking using Modeling Notation of IoT System Architecture Shinpei Ogata (Shinshu Univ.), Yoshitaka Aoki (NUL), Hiroyuki Nakagawa (Osaka Univ.), Kazuki Kobayashi (Shinshu Univ.), Yuko Fukushima (NUL) SS2017-5 KBSE2017-5 |
IoT system architecture often relates to various objects such as users, Web services, edges, devices, energy suppliers a... [more] | SS2017-5 KBSE2017-5 pp.25-30 |
|
[Return to Top Page]