| 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, SS, IPSJ-SE [detail] | 2015-07-23 16:50 |
Hokkaido | Model Checking for UI Specification of RIA with Data Binding Takuya Iwatsuka, Tsuyoshi Oshima, Toshifumi Enomoto (NTT)  SS2015-28 KBSE2015-21 |
RIAs realize a high degree of usability come from partial page rewriting by client-side scripting. Their dynamic nature ... [more] | SS2015-28 KBSE2015-21 pp.137-142 |
|
| 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 |
|
| MSS, CAS, SIP, VLD | 2015-06-18 10:10 |
Hokkaido | Otaru University of Commerce | Software model checking of embedded assembly programs by symbolic execution Ryosuke Konoshita, Satoshi Yamane (Kanazawa Univ.) CAS2015-15 VLD2015-22 SIP2015-46 MSS2015-15 |
We have developed a software verification system for embedded assembly programs. It dynamically generates a model by th... [more] |
CAS2015-15 VLD2015-22 SIP2015-46 MSS2015-15 pp.77-81 |
| 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 |
| CPSY, IPSJ-EMB, IPSJ-SLDM, DC [detail] | 2015-03-07 13:00 |
Kagoshima | Study of Cost Reduction Technique for FPGA-based Control Systems by Quantitative Evaluation of Dangerous Failure Ratio Teppei Hirotsu, Tadanobu Toba (Hitachi) CPSY2014-180 DC2014-106 |
FPGA is one of promising device to gain the performance of embedded systems with the progress of speed-up and cost reduc... [more] | CPSY2014-180 DC2014-106 pp.119-124 |
|
| KBSE | 2015-03-05 14:30 |
Tokyo | The University of Electro-Communications | Investigation of model checking by modular approach, and practicality of modular verification Takumi Miyajima (Ibaraki Univ.), Kei Kogai (INCT), Yoshikazu Ueda (Ibaraki Univ.), Tomoyuki Yamagata, Takayuki Takezawa (Hitachi) KBSE2014-56 |
Model checking to search mechanically and cyclopedically for inspection system is difficult because of exponential incre... [more] | KBSE2014-56 pp.25-30 |
| 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 |
| 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 |
| MSS | 2015-03-06 13:55 |
Ishikawa | IT Business Plaza Musashi | The symbolic model checking by the model extraction from embedded assembly program Tomonori Kato, Ryosuke Konoshita, Kohei Sakurai, Satoshi Yamane (Kanazawa Univ.) MSS2014-102 |
Embedded systems have been widely used. In addition, embedded systems have been gradually complicated.It is important to... [more] | MSS2014-102 pp.65-70 |
| MSS, SS | 2015-01-26 17:20 |
Tottori | A Consideration on How to Model Check Distributed Snapshot Reachability Property Wenjie Zhang, Kazuhiro Ogata (JAIST), Min Zhang (ECNU) MSS2014-77 SS2014-41 |
The Chandy-Lamport Distributed Snapshot Algorithm (CLDSA) can determine a consistent global state (called a snapshot) of... [more] | MSS2014-77 SS2014-41 pp.49-54 |
|
| NLP | 2015-01-26 17:35 |
Oita | Compal Hall | An Application of RRT Algorithm to Reliability Assessment of Energy Systems Yoshihiko Susuki (Kyoto Univ./JST), T. John Koo (ASTRI) NLP2014-128 |
Assessment of reliability related to dynamics of energy systems is formulated as a problem of checking reachability of a... [more] | NLP2014-128 pp.89-94 |
| KBSE | 2015-01-26 14:40 |
Tokyo | Kikai-Shinko-Kaikan Bldg. | An Investigation of a Reverse Engineering Method for Verifying Source Code with a Use Case Model
-- A Case of an ASP.NET Application -- Shinpei Ogata (Shinshu Univ.), Yoshitaka Aoki (SIT), Satoshi Yazawa (VR), Saeko Matsuura (SIT) KBSE2014-42 |
Traceability between a requirements specification and source code should be kept but it’s difficult. Verifying that the ... [more] | KBSE2014-42 pp.19-24 |
| 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 |
| MoNA, CQ (Joint) |
2014-09-12 13:35 |
Miyagi | Performance Evaluation of Device Discovery Time in Bluetooth LE with Probabilistic Model Checking Yusuke Matsuo, Daisuke Umehara, Koichiro Wakasugi (Kyoto Inst. of Tech.) CQ2014-61 |
Pairing in Bluetooth consumes electric energy each device discovery. Since almost all Bluetooth peripherals are battery... [more] |
CQ2014-61 pp.123-128 |
|
| 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 |
| 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-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, 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 |
| 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 |
[Return to Top Page]