Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
SWIM, KBSE |
2023-05-20 14:25 |
Shizuoka |
(Primary: On-site, Secondary: Online) |
A Study on Identifying the Occurrence of User's Forgetting to Take Items from Interactive Systems Ruka Narisawa, Shinpei Ogata (Shinshu Univ.), Yoshitaka Aoki (BIPROGY), Hiroyuki Nakagawa (Osaka Univ.), Kazuki Kobayashi, Kozo Okano (Shinshu Univ.) |
[more] |
|
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 |
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 |
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 |
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, 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 |
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 |
KBSE |
2016-03-03 13:50 |
Oita |
|
Verification of Goal Satisfaction to Combination of Use Case Components Saeko Matsuura (Shibaura Inst. of Tech.), Shinpei Ogata (Shinshu Univ.), Yoshitaka Aoki (Nihon Unisys) KBSE2015-54 |
[more] |
KBSE2015-54 pp.37-42 |
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 |
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 |
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 |
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 |
KBSE |
2014-03-06 10:35 |
Okinawa |
Okinawaken-Seinenkaikan |
A Method for Facilitating the Analysis of Counterexamples in Model Checking Yoshitaka Aoki (Nihon Unisys), Saeko Matsuura (Shibaura Inst. of Tech.) KBSE2013-79 |
[more] |
KBSE2013-79 pp.1-6 |
SS, KBSE |
2013-07-26 13:10 |
Hokkaido |
|
Application to Development Site of Model Checking Technology
-- Discovery of Inconsistency of Specification and Source Code -- Yoshitaka Aoki (Nihon Unisys), Saeko Matsuura (Shibaura Inst. of Tech.) SS2013-28 KBSE2013-28 |
Software programs often include many defects that are not easy to detect because of the developers’ mistakes, misunderst... [more] |
SS2013-28 KBSE2013-28 pp.91-96 |
SS, KBSE |
2013-07-26 13:40 |
Hokkaido |
|
Verification of Feasibility by Model Checking Techniques Applied to UML Requirements Analysis Model Yoshitaka Aoki (Nihon Unisys), Shinpei Ogata (Shinshu Univ.), Saeko Matsuura (Shibaura Inst. of Tech.) SS2013-29 KBSE2013-29 |
A key to success of developing high quality software products is to define valid and feasible requirements specification... [more] |
SS2013-29 KBSE2013-29 pp.97-102 |
KBSE |
2013-03-14 10:05 |
Tokyo |
Shibaura Institute of Technology |
Verification of Program Defects Based on Model Checking Techniques for Development
-- Stable Checking with Inspection Support Tool -- Yoshitaka Aoki (Nihon Unisys), Saeko Matsuura (Shibaura Inst. of Tech.) KBSE2012-69 |
In the development site, difficult defects of detecting occurs when Miss inadequate requirements definition and implem... [more] |
KBSE2012-69 pp.1-6 |
KBSE |
2012-11-23 15:05 |
Ishikawa |
Kanazawa University |
An Automatic Use of Model Checking Tool for Validating Data Lifecycle Shinpei Ogata (Shinshu Univ.), Satoshi Yazawa, Kazuhiko Nishimura (VR), Yoshitaka Aoki, Hirotaka Okuda, Saeko Matsuura (SIT) KBSE2012-56 |
Model checking techniques are a promised technique to detect errors in a specification efficiently and exhaustively. How... [more] |
KBSE2012-56 pp.109-114 |
WIT |
2012-01-28 14:30 |
Aichi |
Nagoya Institute of Technology |
Development of simplified repeated resistance training system for severe hemiparetic stroke patient Yoshifumi Morita, Yuki Iida, Yuki Hiramatsu, Michito Yasukita, Kazunori Yamazaki, Noritaka Sato, Hiroyuki Ukai (Nagoya Inst. Tech.), Yoshiaki Takagi, Yoshitaka Aoki (Sanyo Machine Works), Hirofumi Tanabe, Rumi Tanemura (Kobe Univ.) WIT2011-64 |
[more] |
WIT2011-64 pp.67-72 |
KBSE |
2012-01-23 16:20 |
Tokyo |
Kikai-Shinko-Kaikan Bldg. |
A Method for Detecting Defects of Program Based on Model Checking Techniques for Development Site Yoshitaka Aoki (NUL), Saeko Matsuura (S.I.T) KBSE2011-60 |
[more] |
KBSE2011-60 pp.43-48 |