Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
KBSE |
2024-03-14 13:45 |
Okinawa |
Okinawa Prefectual General Welfare Center (Primary: On-site, Secondary: Online) |
Consideration on System Safety Verification Based on User Personality Traits Ruka Narisawa, Shinpei Ogata (Shinshu Univ.), Yoshitaka Aoki (BIPROGY), Hiroyuki Nakagawa (Osaka Univ.), Kazuki Kobayashi, Kozo Okano (Shinshu Univ.) KBSE2023-72 |
(To be available after the conference date) [more] |
KBSE2023-72 pp.43-48 |
KBSE |
2024-03-14 14:10 |
Okinawa |
Okinawa Prefectual General Welfare Center (Primary: On-site, Secondary: Online) |
Applying Model Checking to Ethical Judgments Yoshitaka Aoki, Yotaro Nakayama (BIPROGY) KBSE2023-73 |
(To be available after the conference date) [more] |
KBSE2023-73 pp.49-54 |
DC |
2024-02-28 11:20 |
Tokyo |
Kikai-Shinko-Kaikan Bldg. |
DC2023-96 |
(To be available after the conference date) [more] |
DC2023-96 pp.11-16 |
SS, DC |
2023-10-11 16:00 |
Nagano |
(Primary: On-site, Secondary: Online) |
Formal Verification of Concurrent Algorithms: Case Studies on Mutual Exclusion Naoki Nishiguchi, Tatsuhiro Tsuchiya (Osaka Univ.) SS2023-24 DC2023-30 |
(To be available after the conference date) [more] |
SS2023-24 DC2023-30 pp.19-21 |
SWIM, KBSE |
2023-05-20 14:25 |
Shizuoka |
(Primary: On-site, Secondary: Online) |
A Study on Identifying 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.) KBSE2023-10 SWIM2023-10 |
(To be available after the conference date) [more] |
KBSE2023-10 SWIM2023-10 pp.59-64 |
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 |
SS |
2023-03-15 09:55 |
Okinawa |
(Primary: On-site, Secondary: Online) |
Regularity Preservation Property of Data Tree Rewrite Systems
-- A Subclass Decomposable into Monadic Normal Form -- Yuto Sakao, Hiroyuki Seki (Nagoya Univ.) SS2022-62 |
Let $T$ be a transformation over a class $mathcal{L}$ of languages. If for any regular language $L in mathcal{L}$, $T^*(... [more] |
SS2022-62 pp.91-96 |
KBSE |
2023-01-19 15:10 |
Ishikawa |
(Primary: On-site, Secondary: Online) |
Fujimoto Masaya, Nakagawa Hiroyuki, Tsuchiya Tatsuhiro (Osaka Univ.) KBSE2022-47 |
(To be available after the conference date) [more] |
KBSE2022-47 pp.25-30 |
KBSE, SC |
2022-11-05 09:30 |
Nagano |
(Primary: On-site, Secondary: Online) |
Analysis of Parrondo's Paradox using a probabilistic model checker Naoki Nishiguchi, Hiroyuki Nakagawa, Tatsuhiro Tsuchiya (Osaka Univ.) KBSE2022-38 SC2022-33 |
(To be available after the conference date) [more] |
KBSE2022-38 SC2022-33 pp.43-47 |
MSS, NLP |
2022-03-28 10:05 |
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 pp.13-18 |
MSS, NLP |
2022-03-29 14:55 |
Online |
Online |
Verification of spacecraft operational scenario using Little-JIL Kazunori Someya (JAXA), Kunihiko Hiraishi (JAIST) MSS2021-78 NLP2021-149 |
Inadequate operational scenario leads to satellite loss in the case of the operational accident of the X-ray astronomy s... [more] |
MSS2021-78 NLP2021-149 pp.121-126 |
SS, DC |
2021-10-19 15:25 |
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 pp.23-28 |
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 |
SS |
2021-03-03 10:25 |
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] |
SS2020-29 pp.7-12 |
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 |
SS |
2020-03-05 12:05 |
Okinawa |
(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 pp.93-98 |
ICSS, IPSJ-SPT |
2020-03-03 11:00 |
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 pp.119-124 |
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 |