Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
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 |
MSS |
2017-03-16 11:20 |
Shimane |
Shimane Univ. |
Verification Methods of real-time properties for embedded assembly program
-- Model checking and deductive verification for embedded program -- Satoshi Yamane (Kanazawa Univ.) MSS2016-83 |
It is important to verify both the correctness and real-time properties for embedded systems.
In this paper, we propos... [more] |
MSS2016-83 pp.11-16 |
SS |
2017-03-10 09:15 |
Okinawa |
|
Detecting Anormal Power Consumption in a Concurrent of Android Application Takahiro Inagaki, Shoji Yuen (Nagoya Univ.) SS2016-74 |
We propose a method for an automatic detection of the power consumption problem in concurrent execution of Android appli... [more] |
SS2016-74 pp.85-90 |
KBSE |
2017-03-03 12:50 |
Ishikawa |
|
KBSE2016-40 |
Self-adaptive systems, which change their behaviors to adapt to their environmental changes, are focused on in recent ye... [more] |
KBSE2016-40 pp.7-12 |
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 |
MBE |
2016-07-30 14:30 |
Okayama |
Okayama University |
Development of a management system for ventilators Takayuki Torigoe, Hisashi Miyazaki (Kawasaki Univ. of Medical Welfare), Saya Danjo (Rakuwakai Healthcare System Otowa Hosp.), Isao Kayano (Kawasaki Univ. of Medical Welfare), Yasuo Ogasawara (Kawasaki Med. Sch./Kawasaki Univ. of Medical Welfare) MBE2016-18 |
A ventilator is one of the life-support devices that are centrally managed in hospitals. Maintenance and checking of ve... [more] |
MBE2016-18 pp.17-20 |
KBSE, SS, IPSJ-SE [detail] |
2016-07-13 10:20 |
Hokkaido |
|
A Method to Revise Message Ordering in Sequence Diagram Kozo Okano (Shinshu Univ.), Satoshi Harauchi (Mitsubishi Electric Corp.), Yosuke Tajima, Shinpei Ogata (Shinshu Univ.) SS2016-2 KBSE2016-8 |
For software specification, a lot of methods have been proposed in order to localize defects and to fix
defects automat... [more] |
SS2016-2 KBSE2016-8 pp.7-12 |
MBE |
2016-06-17 13:25 |
Hokkaido |
Hokkaido University |
Verification of a management system for ventilator using model checking Hisashi Miyazaki, Takayuki Torigoe, Isao Kayano (Kawasaki Univ of Medical Welfare), Yasuo Ogasawara (Kawasaki Medical School/Kawasaki Univ of Medical Welfare) MBE2016-14 |
In a hospital, medical staffs may be used a system which is developed by themselves for promotion of streamlining and im... [more] |
MBE2016-14 pp.27-30 |
KBSE |
2016-05-27 10:45 |
Tokyo |
Doshisha Univ. Tokyo Branch Office |
Model Checking of Source Code Based on Design Pattern Yoshitaka Aoki (NUL) KBSE2016-6 |
We have proposed the " Discovery of Inconsistency of Behavior of System in Source Code between Specification using Model... [more] |
KBSE2016-6 pp.31-36 |
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 |
MSS |
2016-03-03 10:30 |
Yamaguchi |
KAIKYO MESSE SHIMONOSEKI |
Analysis of Boundedness and Liveness for Agent-Oriented Petri Net PN^2 and its Application for IoT Services Shoki Tsugawa, Kazuya Nakahori, Shingo Yamaguchi (Yamaguchi Univ.) MSS2015-67 |
In this paper, we regard a service as a multi-agent system, and represent it as an agent-oriented Petri net, called Petr... [more] |
MSS2015-67 pp.1-4 |
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 11:45 |
Ishikawa |
Shiinoki-Geihin-Kan |
Application of Transition Predicate Abstraction to Non-Zeno Fairness Verification for Linear Hybrid Automaton Ryo Yanase, Satoshi Yamane (Kanazawa Univ.) MSS2015-40 SS2015-49 |
For verifying fairness properties of a hybrid system, in generally, it is necessary to show that the system also satisfi... [more] |
MSS2015-40 SS2015-49 pp.29-33 |
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 |
SS, MSS |
2016-01-25 18:30 |
Ishikawa |
Shiinoki-Geihin-Kan |
A Study of a Practical Approach to Verifying Control Systems using Model-Checking and Testing Junya Matsubara, Rieko Takagi, Teruyuki Nakazawa (Denso Create), Tetsuya Tohdo, Hiroyuki Ihara, Yukinori Kawaai (Denso) MSS2015-52 SS2015-61 |
Due to the automotive control systems have become complex, it is necessary to ensure the dependability of the systems. I... [more] |
MSS2015-52 SS2015-61 pp.99-103 |
CS, OCS (Joint) |
2016-01-22 11:15 |
Kagoshima |
Kagoshima University, Korimoto Campus, Inamori Auditorium |
Performance Evaluation of Bluetooth LE Device Discovery on Simultaneous Multiple Access Yusuke Matsuo, Disuke Umehara (Kyoto Inst. of Tech.), Hidekazu Murata (Kyoto Univ.), Satoshi Denno (Okayama Univ.) CS2015-83 |
Bluetooth BR/EDR (Basic Rate/Enhanced Data Rate) has a technical issue on energy consumption when slaves join the networ... [more] |
CS2015-83 pp.61-66 |