| 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 | 2023-03-17 10:40 |
Hiroshima | JMS ASTERPLAZA (Primary: On-site, Secondary: Online) |
Verification of Interaction between Functions in FRAM using Model Checking Yoshitaka Aoki (BIPROGY), Kenji Hisazumi (Shibaura Inst. of Tech.)  KBSE2022-62 |
Analysis of FRAM models tends to rely on the domain knowledge of analysts, and it is difficult for anyone to evaluate co... [more] | KBSE2022-62 pp.49-54 |
| KBSE | 2023-03-17 12:50 |
Hiroshima | JMS ASTERPLAZA (Primary: On-site, Secondary: Online) |
On Family-based Model Checking based on Probabilistic Model Checker Tomoji Kishi (Waseda Univ) KBSE2022-64 |
Family-based model checking is a technique to verify the properties of multiple product variations at once by performing... [more] | KBSE2022-64 pp.61-66 |
| 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 |
| 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 |
| 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] | 2016-11-24 13:25 |
Hyogo | Kobe Institute of Computing | Development and evaluation of on-the-fly model checking for a Petri net verification tool (HiPS) Yojiro Harie, Katsumi Wasaki (Shinshu Univ.) CAS2016-63 MSS2016-43 |
This paper proposes an On-the-fly Fluent Linear Temporal Logic (FLTL) model checker using state space generation based o... [more] | CAS2016-63 MSS2016-43 pp.31-35 |
| SS | 2016-03-11 14:15 |
Okinawa | Towards Behavior Verification of Estimation of Self-localization in One-dimensional Systems Toshifusa Sekizawa (Nihon Univ.), Kozo Okano (Shinshu Univ.) SS2015-100 |
Along with the popularization of embedded systems in society, reliability of them has become important. Model checking i... [more] | SS2015-100 pp.145-150 |
|
| KBSE | 2016-03-03 15:20 |
Oita | [Invited Talk]
Model-Driven Development Embracing Uncertainty Naoyasu Ubayashi (Kyushu Univ.) KBSE2015-56 |
Embracing uncertainty in software development is one of the crucial research topics in software engineering. Garlan, D. ... [more] | KBSE2015-56 p.49 |
|
| VLD | 2016-02-29 13:30 |
Okinawa | Okinawa Seinen Kaikan | Tool Support for Verifying Large Scale Hardware Design with Verilog-HDL Yuta Morimitsu, Tomoyuki Yokogawa (Okayama Prefectural Univ.), Masafumi Kondo, Hisashi Miyazaki (Kawasaki Univ. of Medical Welfare), Yoichiro Sato, Kazutami Arimoto (Okayama Prefectural Univ.), Norihiro Yoshida (Nagoya Univ.) VLD2015-111 |
In this paper, we developed a tool supporting formal verification of large scale hardware design described by Verilog-HD... [more] | VLD2015-111 pp.1-6 |
| SS, MSS | 2016-01-25 15:45 |
Ishikawa | Shiinoki-Geihin-Kan | On-the-fly Model Checker for a Petri Net Verification Tool(HiPS) by using Replacement LTL Formula to Event-Based Automaton Yojiro Harie, Katsumi Wasaki (Shinshu Univ.) MSS2015-46 SS2015-55 |
This paper proposes an On-the-fly Linear Temporal Logic (LTL) model checker using state space generation based on the Pe... [more] | MSS2015-46 SS2015-55 pp.63-68 |
| KBSE, SS, IPSJ-SE [detail] | 2015-07-24 11:40 |
Hokkaido | Applying Model Checking on VDM Models using SPIN Hsin-Hung Lin, Yoichi Omori, Shigeru Kusakabe, Keijiro Araki (Kyushu Univ.) SS2015-34 KBSE2015-27 |
The Vienna Development Method (VDM) is a formal method which supports modeling and analysis of software systems at vario... [more] | SS2015-34 KBSE2015-27 pp.173-178 |
|
| SS | 2015-03-09 13:25 |
Okinawa | OKINAWAKEN SEINENKAIKAN | Statistical Model Checking with Adaptive Importance Sampling Yu Nishiki, Shoji Yuen (Nagoya Univ) SS2014-61 |
We propose a method for statitical model checking of error as rare events with adaptive importance sampling, where the f... [more] | SS2014-61 pp.37-42 |
| SS | 2015-03-09 13:50 |
Okinawa | OKINAWAKEN SEINENKAIKAN | Removing Possibility of Ambiguous Message Ordering in Sequence Diagram Noa Kusunoki, Kozo Okano, Shinji Kusumoto (Osaka Univ.) SS2014-62 |
This report proposes a method to detect and repair software faults in sequence diagrams which are used for software desi... [more] | SS2014-62 pp.43-48 |
| MSS | 2015-03-06 10:25 |
Ishikawa | IT Business Plaza Musashi | Development of SMT-based model checker for assembly cords using interrupts reduction technique Junpei Kobashi, Atsushi Takeshita, Satoshi Yamane, Kohei Sakurai (Kanazawa Univ.) MSS2014-100 |
Recently, embedded software has properties dependent on hardware (direct operation of address spaces, memory mapped I/O,... [more] | MSS2014-100 pp.53-58 |
| CPSY, DC (Joint) |
2014-07-29 15:40 |
Niigata | Toki Messe, Niigata | Evaluation of Large-scale Graph Rewriting Model Checking Using Hash Compaction Taketo Yoshida, Masaru Onuma, Kazunori Ueda (Waseda Univ.) DC2014-19 |
Graph rewriting model checking is a verification method that determines whether a model described in a graph rewriting s... [more] | DC2014-19 pp.9-16 |
| KBSE, SS, IPSJ-SE [detail] | 2014-07-11 13:10 |
Hokkaido | Furano-Bunka-Kaikan | On Coverage Criteria for State Transition Testing and Model Checker-Based Test Case Generation Cassia de Souza Carvalho, Tatsuhiro Tsuchiya (Osaka Univ.) SS2014-23 KBSE2014-26 |
State Transition Testing is an important category of software testing. Our work in progress focuses on a coverage crit... [more] |
SS2014-23 KBSE2014-26 pp.149-154 |
| SS | 2014-03-11 13:00 |
Okinawa | Tenbusu Naha | Analyzing Requirememts Sentences for Checking Use Case Descriptions Ryotaro Nakamura, Shinpei Hayashi, Motoshi Saeki (Tokyo Tech.) SS2013-76 |
Since use case descriptions written in a natural language are informal, it is difficult to analyze them automatically. T... [more] | SS2013-76 pp.25-30 |
| VLD | 2014-03-05 15:45 |
Okinawa | Okinawa Seinen Kaikan | A Case Study of Symbolic Model Checking for Verilog-HDL Hardware Design Tomoyuki Yokogawa, Daichi Higashiyama (Okayama Pref. Univ.), Masafumi Kondo (Kawasaki Univ. of Medical Welfare), Yoichiro Sato, Kazutami Arimoto (Okayama Pref. Univ.) VLD2013-166 |
In this paper, we show a case study where a design of 8bit microcomputer M8R, which is described by Verilog-HDL, is veri... [more] | VLD2013-166 pp.177-182 |
| KBSE | 2012-11-23 13:40 |
Ishikawa | Kanazawa University | Applying SPIN to operation manuals to prevent system fault Tsutomu Miyazaki, Atsuo Ohki, Takako Nakatani (GSSM,Univ. of Tsukuba) KBSE2012-54 |
In order to prevent system fault, it is important to improve the quality of system operations in the same way as that of... [more] | KBSE2012-54 pp.97-102 |
| SS, IPSJ-SE | 2012-11-01 13:40 |
Hiroshima | Hiroshima City University | A discussion of fault patterns for concurrent systems Han-Myung Chang, Masami Noro, Atsushi Sawada, Atsushi Yoshida, Yoshinari Hachisu, Reishi Yokomori (Nanzan Univ.) SS2012-40 |
In model checking, when a model checker fails to verify deadlock free, or some safety property or liveness property, its... [more] | SS2012-40 pp.41-46 |
[Return to Top Page]