IEICE Technical Committee Submission System
Conference Schedule
Online Proceedings
[Sign in]
Tech. Rep. Archives
    [Japanese] / [English] 
( Committee/Place/Topics  ) --Press->
( Paper Keywords:  /  Column:Title Auth. Affi. Abst. Keyword ) --Press->

All Technical Committee Conferences  (Searched in: All Years)

Search Results: Conference Papers
 Conference Papers (Available on Advance Programs)  (Sort by: Date Descending)
 Results 1 - 20 of 144  /  [Next]  
Committee Date Time Place Paper Title / Authors Abstract Paper #
SS, IPSJ-SE, KBSE [detail] 2022-07-29
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
MSS, NLP 2022-03-28
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
SS, DC 2021-10-19
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
ITS, IEE-ITS 2021-03-15
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
SS 2021-03-03
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]
SS 2021-03-04
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]
DC, SS 2020-10-19
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
KBSE 2020-03-06
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
SS 2020-03-05
(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
ICSS, IPSJ-SPT 2020-03-03
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
KBSE, SC 2019-11-08
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
SWIM, KBSE 2019-05-25
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
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]
SS 2019-03-04
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
SS 2019-03-05
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
MSS, CAS, IPSJ-AL [detail] 2018-11-13
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
KBSE, SS, IPSJ-SE [detail] 2018-07-18
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
SS 2018-03-06
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]
SS, KBSE, IPSJ-SE [detail] 2017-07-19
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
SS, KBSE, IPSJ-SE [detail] 2017-07-19
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
 Results 1 - 20 of 144  /  [Next]  
Choose a download format for default settings. [NEW !!]
Text format pLaTeX format CSV format BibTeX format
Copyright and reproduction : All rights are reserved and no part of this publication may be reproduced or transmitted in any form or by any means, electronic or mechanical, including photocopy, recording, or any information storage and retrieval system, without permission in writing from the publisher. Notwithstanding, instructors are permitted to photocopy isolated articles for noncommercial classroom use without fee. (License No.: 10GA0019/12GB0052/13GB0056/17GB0034/18GB0034)

[Return to Top Page]

[Return to IEICE Web Page]

The Institute of Electronics, Information and Communication Engineers (IEICE), Japan