Toshiaki Aoki

Publication Activity (10 Years)

Years Active: 1998-2023
Publications (10 Years): 44

Top Topics

Interval Arithmetic

Fault Tree Analysis

Systematic Evaluation

Formal Specification

Top Venues

IEICE Trans. Inf. Syst.

Publications

Yuki Yamaguchi, Toshiaki Aoki
Attack Tree Analysis for Adversarial Evasion Attacks. CoRR (2023)
Kento Tanaka, Toshiaki Aoki, Tatsuji Kawai, Takashi Tomita, Daisuke Kawakami, Nobuo Chida
Specification Based Testing of Object Detection for Automated Driving Systems via BBSL. ENASE (2023)
Kazunori Someya, Toshiaki Aoki, Naoki Ishihama
Compaction of Spacecraft Operational Models with Metamodeling Domain Knowledge. ENASE (2023)
Yuki Yamaguchi, Toshiaki Aoki
Attack Tree Analysis for Adversarial Evasion Attacks. PRDC (2023)
Toshiaki Aoki, Aritoshi Hata, Kazusato Kanamori, Satoshi Tanaka, Yuta Kawamoto, Yasuhiro Tanase, Masumi Imai, Fumiya Shigemitsu, Masaki Gondo, Tomoji Kishi
Model-Checking in the Loop Model-Based Testing for Automotive Operating Systems. CoRR (2023)
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki
Approximate Translation from Floating-Point to Real-Interval Arithmetic. NFM (2022)
Toshiaki Aoki, Qin Li
Selected papers from the 14th international symposium on Theoretical Aspects of Software Engineering. Sci. Comput. Program. 219 (2022)
Charnon Pattiyanon, Toshiaki Aoki, Daisuke Ishii
A Method for Detecting Common Weaknesses in Self-Sovereign Identity Systems Using Domain-Specific Models and Knowledge Graph. MODELSWARD (2022)
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai
SMT-Based Model Checking of Industrial Simulink Models. ICFEM (2022)
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai
Coverage Testing of Industrial Simulink Models using Monte-Carlo and SMT-Based Methods. QRS (2022)
Thuy Nguyen, Takashi Tomita, Junpei Endo, Geon-ung Kang, Toshiaki Aoki
Leveraging hardware-dependent knowledge extraction with multiple program analysis techniques. SAC (2022)
Kento Tanaka, Toshiaki Aoki, Tatsuji Kawai, Takashi Tomita, Daisuke Kavvakami, Nobuo Chida
A Formal Specification Language Based on Positional Relationship Between Objects in Automated Driving Systems. COMPSAC (2022)
Charnon Pattiyanon, Toshiaki Aoki
Compliance SSI System Property Set to Laws, Regulations, and Technical Standards. IEEE Access 10 (2022)
Charnon Pattiyanon, Toshiaki Aoki
Analysis and Enhancement of Self-sovereign Identity System Properties Compiling Standards and Regulations. ICISSP (2022)
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai
SMT-Based Model Checking of Industrial Simulink Models. CoRR (2022)
Jingcheng Yuan, Toshiaki Aoki, Xiaoyun Guo
Comprehensive evaluation of file systems robustness with SPIN model checking. Softw. Test. Verification Reliab. 32 (6) (2022)
Daisuke Ishii, Takashi Tomita, Toshiaki Aoki
Approximate Translation from Floating-Point to Real-Interval Arithmetic. CoRR (2021)
Thuy Nguyen, Takashi Tomita, Junpei Endo, Toshiaki Aoki
Integrating pattern matching and abstract interpretation for verifying cautions of microcontrollers. Softw. Test. Verification Reliab. 31 (8) (2021)
Daisuke Ishii, Takashi Tomita, Kenji Onishi, Toshiaki Aoki
Compositional Test Generation of Industrial Synchronous Systems. CoRR (2021)
Nhat-Hoa Tran, Toshiaki Aoki
SSpinJa: Facilitating Schedulers in Model Checking. QRS (2021)
Toshiaki Aoki, Daisuke Kawakami, Nobuo Chida, Takashi Tomita
Dataset Fault Tree Analysis for Systematic Evaluation of Machine Learning Systems. PRDC (2020)
Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki
Template-Based Monte-Carlo Test-Suite Generation for Large and Complex Simulink Models. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. (2) (2020)
Xiaoyun Guo, Toshiaki Aoki, Hsin-Hung Lin
Model checking of in-vehicle networking systems with CAN and FlexRay. J. Syst. Softw. 161 (2020)
Kenji Fujita, Kunihiko Hiraishi, Toshiaki Aoki
Frequency Probabilistic Risk Assessment Using Coloured Petri Nets for Telemedicine. IEEM (2020)
Hoang-Viet Tran, Pham Ngoc Hung, Viet-Ha Nguyen, Toshiaki Aoki
A framework for assume-guarantee regression verification of evolving software. Sci. Comput. Program. 193 (2020)
Jingcheng Yuan, Toshiaki Aoki, Xiaoyun Guo
Comprehensive Robustness Evaluation of File Systems with Model Checking. QRS (2020)
Thu Trang Nguyen, Pattaravut Maleehuan, Toshiaki Aoki, Takashi Tomita, Iori Yamada
Reducing false positives of static analysis for SEI CERT C coding standard. CESSER-IP@ICSE (2019)
Nhat-Hoa Tran, Yuki Chiba, Toshiaki Aoki
Model Checking in the Presence of Schedulers Using a Domain-Specific Language for Scheduling Policies. IEICE Trans. Inf. Syst. (7) (2019)
Toshiaki Aoki
Foreword. IEICE Trans. Inf. Syst. (8) (2019)
Thu-Trang Nguyen, Toshiaki Aoki, Takashi Tomita, Iori Yamada
Multiple Program Analysis Techniques Enable Precise Check for SEI CERT C Coding Standard. APSEC (2019)
Nhat-Hoa Tran, Toshiaki Aoki
Conformance Testing of Schedulers for DSL-based Model Checking. SPIN (2019)
Thuy Nguyen, Toshiaki Aoki, Takashi Tomita, Junpei Endo
Integrating Static Program Analysis Tools for Verifying Cautions of Microcontroller. APSEC (2019)
Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki
A scalable Monte-Carlo test-case generation tool for large and complex simulink models. MiSE@ICSE (2019)
Nhat-Hoa Tran, Yuki Chiba, Toshiaki Aoki
Qualitative and quantitative analysis with scheduling policies in model checking. SAC (2018)
Zhengguo Yang, Toshiaki Aoki, Yasuo Tan
Multiple Conformance to Hybrid Automata for Checking Smart House Temperature Change. DS-RT (2018)
Zhengguo Yang, Toshiaki Aoki, Yasuo Tan
Modeling the Required Indoor Temperature Change by Hybrid Automata for Detecting Thermal Problems. PRDC (2018)
Khanh Trinh Le, Yuki Chiba, Toshiaki Aoki
Formalization and Verification of AUTOSAR OS Standard's Memory Protection. TASE (2018)
Pattaravut Maleehuan, Yuki Chiba, Toshiaki Aoki
A Verification Framework for Assembly Programs Under Relaxed Memory Model Using SMT Solver. IEICE Trans. Inf. Syst. (12) (2018)
Xiaoyun Guo, Hsin-Hung Lin, Toshiaki Aoki, Yuki Chiba
A Reusable Framework for Modeling and Verifying In-Vehicle Networking Systems in the Presence of CAN and FlexRay. APSEC (2017)
Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki
Template-Based Monte-Carlo Test Generation for Simulink Models. CyPhy (2017)
Nhat-Hoa Tran, Yuki Chiba, Toshiaki Aoki
Domain-Specific Language Facilitates Scheduling in Model Checking. APSEC (2017)
Pattaravut Maleehuan, Yuki Chiba, Toshiaki Aoki
Assembly program verification for multiprocessors with relaxed memory model using SMT solver. TASE (2017)
Min Zhang, Toshiaki Aoki, Yueying He
A spiral process of formalization and verification: A case study on verification of the scheduling mechanism of OSEK/VDX. J. Inf. Secur. Appl. 31 (2016)
Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
Verifying OSEK/VDX OS Design Using Its Formal Specification. TASE (2016)
Hideto Ogawa, Makoto Ichii, Fumihiro Kumeno, Toshiaki Aoki
Experimental Fault Analysis Process Implemented Using Model Extraction and Model Checking. COMPSAC (2015)
Toshiaki Aoki, Kriangkrai Traichaiyaporn, Yuki Chiba, Masahiro Matsubara, Masataka Nishi, Fumio Narisawa
Modeling Safety Requirements of ISO26262 Using Goal Trees and Patterns. FTSCS (2015)
Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
A Framework for Verifying the Conformance of Design to Its Formal Specifications. IEICE Trans. Inf. Syst. (6) (2015)
Haitao Zhang, Toshiaki Aoki, Yuki Chiba
Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications. ICST (2015)
Haitao Zhang, Toshiaki Aoki, Yuki Chiba
Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach. IEICE Trans. Inf. Syst. (10) (2015)
Haitao Zhang, Toshiaki Aoki, Yuki Chiba
A Spin-Based Approach for Checking OSEK/VDX Applications. FTSCS (2014)
Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki
Checking the Conformance of a Promela Design to its Formal Specification in Event-B. FTSCS (2014)
Shinji Kikuchi, Toshiaki Aoki
Evaluation of Operational Vulnerability in Cloud Service Management Using Model Checking. SOSE (2013)
Kriangkrai Traichaiyaporn, Toshiaki Aoki
Refinement Tree and Its Patterns: A Graphical Approach for Event-B Modeling. FTSCS (2013)
Xiaoyun Guo, Hsin-Hung Lin, Kenro Yatake, Toshiaki Aoki
An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol. FTSCS (2013)
Kenji Taguchi, Hideaki Nishihara, Toshiaki Aoki, Fumihiro Kumeno, Koji Hayamizu, Koichi Shinozaki
Building a Body of Knowledge on Model Checking for Software Development. COMPSAC (2013)
Hideto Ogawa, Makoto Ichii, Fumihiko Kumeno, Toshiaki Aoki
A Practical Study of Debugging Using Model Checking. APSEC (2) (2013)
Haitao Zhang, Toshiaki Aoki, Kenro Yatake, Min Zhang, Hsin-Hung Lin
An Approach for Checking OSEK/VDX Applications. QSIC (2013)
Kriangkrai Traichaiyaporn, Toshiaki Aoki
Preserving Correctness of Requirements Evolution through Refinement in Event-B. APSEC (1) (2013)
Haitao Zhang, Toshiaki Aoki, Hsin-Hung Lin, Min Zhang, Yuki Chiba, Kenro Yatake
SMT-Based Bounded Model Checking for OSEK/VDX Applications. APSEC (1) (2013)
Hirokazu Yatsu, Takahiro Ando, Weiqiang Kong, Kenji Hisazumi, Akira Fukuda, Toshiaki Aoki, Kokichi Futatsugi
Towards Formal Description of Standards for Automotive Operating Systems. ICST Workshops (2013)
Kenro Yatake, Toshiaki Aoki
Model Checking of OSEK/VDX OS Design Model Based on Environment Modeling. ICTAC (2012)
Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama
On Optimization of Minimized Assumption Generation Method for Component-Based Software Verification. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. (9) (2012)
Dieu-Huong Vu, Toshiaki Aoki
Faithfully formalizing OSEK/VDX operating system specification. SoICT (2012)
Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama
Automated Adaptor Generation for Behavioral Mismatching Services Based on Pushdown Model Checking. IEICE Trans. Inf. Syst. (7) (2012)
Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama
An Improvement of Minimized Assumption Generation Method for Component-Based Software Verification. RIVF (2012)
Hiroaki Tanizaki, Toshiaki Aoki, Takuya Katayama
A Variability Management Method for Software Configuration Files. SEKE (2012)
Kenro Yatake, Toshiaki Aoki
SMT-based enumeration of object graphs from UML class diagrams. ACM SIGSOFT Softw. Eng. Notes 37 (4) (2012)
Jiang Chen, Toshiaki Aoki
Conformance Testing for OSEK/VDX Operating System Using Model Checking. APSEC (2011)
Warawoot Pacharoen, Toshiaki Aoki, Athasit Surarerks, Pattarasinee Bhattarakosol
Conformance Verification between Web Service Choreography and Implementation Using Learning and Model Checking. ICWS (2011)
Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama
Automated Adaptor Generation for Services Based on Pushdown Model Checking. ECBS (2011)
Chaiwat Sathawornwichit, Toshiaki Aoki, Takuya Katayama
Modeling of Real-Time System Designs for Parametric Analysis. RTCSA (2010)
Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama
A Minimized Assumption Generation Method for Component-Based Software Verification. IEICE Trans. Inf. Syst. (8) (2010)
Kenro Yatake, Toshiaki Aoki
Automatic Generation of Model Checking Scripts Based on Environment Modeling. SPIN (2010)
Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama
Non-regular Adaptation of Services Using Model Checking. ISORC (2010)
Toshiaki Aoki, Tadashi Sekiguchi, Masayuki Hirayama, Tomoji Kishi
Detecting and Analyzing State Inconsistencies in Multi-task Software. ISORC (2009)
Hideaki Nishihara, Koichi Shinozaki, Koji Hayamizu, Toshiaki Aoki, Kenji Taguchi, Fumihiro Kumeno
Model checking education for software engineers in Japan. ACM SIGCSE Bull. 41 (2) (2009)
Pham Ngoc Hung, Toshiaki Aoki, Takuya Katayama
Modular Conformance Testing and Assume-Guarantee Verification for Evolving Component-Based Software. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. (11) (2009)
Pham Ngoc Hung, Toshiaki Aoki, Takuya Katayama
An effective framework for assume-guarantee verification of evolving component-based software. EVOL/IWPSE (2009)
Pham Ngoc Hung, Toshiaki Aoki, Takuya Katayama
A Minimized Assumption Generation Method for Component-Based Software Verification. ICTAC (2009)
Yasuyuki Tahara, Nobukazu Yoshioka, Kenji Taguchi, Toshiaki Aoki, Shinichi Honiden
Evolution of a course on model checking for practical applications. ACM SIGCSE Bull. 41 (2) (2009)
Toshiaki Aoki
Model Checking Multi-Task Software on Real-Time Operating Systems. ISORC (2008)
Jaejoon Lee, Isabel John, Toshiaki Aoki, John D. McGregor
SPLC 2007 Dectoral Symposium. SPLC (2) (2007)
Toshiaki Aoki, Takuya Katayama
Statechart-based Verification of Object-Oriented Design Models. APSEC (2007)
Takuya Katayama, Tatsuo Nakajima, Taiichi Yuasa, Tomoji Kishi, Shin Nakajima, Shuichi Oikawa, Masahiro Yasugi, Toshiaki Aoki, Mitsutaka Okazaki, Seiji Umatani
Highly Reliable Embedded Software Development Using Advanced Software Technologies. IEICE Trans. Inf. Syst. (6) (2005)
Toshiaki Aoki, Takuya Katayama
Formalization and Analysis of Dataflow in Object-Oriented Design Models. ISORC (2005)
Kenro Yatake, Toshiaki Aoki, Takuya Katayama
Implementing Application-Specific Object-Oriented Theories in HOL. ICTAC (2005)
Kenro Yatake, Toshiaki Aoki, Takuya Katayama
Collaboration-based verification of Object-Oriented models in HOL. VVEIS (2004)
Tomoji Kishi, Toshiaki Aoki, Shin Nakajima, Natsuko Noda, Takuya Katayama
Project Report: High-Reliable Object-Oriented Embedded Software Design. WSTFEUS (2004)
Toshiaki Aoki, Takuya Katayama
Foundations for Evolutionary Construction of State Transition Models. IWPSE (2004)
Mitsutaka Okazaki, Toshiaki Aoki, Takuya Katayama
Extracting threads from concurrent objects for the design of embedded systems. APSEC (2002)
Toshiaki Aoki, Takaaki Tateishi, Takuya Katayama
An Axiomatic Formalization of UML Models. pUML (2001)
Toshiaki Aoki, Takuya Katayama
Unification and Consistency Verification of Object-Oriented Analysis Models. APSEC (1998)