Unification and Consistency Verification of Object-Oriented Analysis Models. - Toshiaki Aoki; Takuya Katayama (APSEC, 1998)

An Axiomatic Formalization of UML Models. - Toshiaki Aoki; Takaaki Tateishi; Takuya Katayama (pUML, 2001)

Extracting threads from concurrent objects for the design of embedded systems. - Mitsutaka Okazaki; Toshiaki Aoki; Takuya Katayama (APSEC, 2002)

Foundations for Evolutionary Construction of State Transition Models. - Toshiaki Aoki; Takuya Katayama (IWPSE, 2004)

Collaboration-based verification of Object-Oriented models in HOL. - Kenro Yatake; Toshiaki Aoki; Takuya Katayama (VVEIS, 2004)

Project Report: High-Reliable Object-Oriented Embedded Software Design. - Tomoji Kishi; Toshiaki Aoki; Shin Nakajima 001; Natsuko Noda; Takuya Katayama (WSTFEUS, 2004)

Implementing Application-Specific Object-Oriented Theories in HOL. - Kenro Yatake; Toshiaki Aoki; Takuya Katayama (ICTAC, 2005)

Formalization and Analysis of Dataflow in Object-Oriented Design Models. - Toshiaki Aoki; Takuya Katayama (ISORC, 2005)

Highly Reliable Embedded Software Development Using Advanced Software Technologies. - Takuya Katayama; Tatsuo Nakajima; Taiichi Yuasa; Tomoji Kishi; Shin Nakajima 001; Shuichi Oikawa; Masahiro Yasugi; Toshiaki Aoki; Mitsutaka Okazaki; Seiji Umatani (IEICE Trans. Inf. Syst., 2005)

Statechart-based Verification of Object-Oriented Design Models. - Toshiaki Aoki; Takuya Katayama (APSEC, 2007)

SPLC 2007 Dectoral Symposium. - Jaejoon Lee; Isabel John; Toshiaki Aoki; John D. McGregor (SPLC (2), 2007)

Model Checking Multi-Task Software on Real-Time Operating Systems. - Toshiaki Aoki (ISORC, 2008)

A Minimized Assumption Generation Method for Component-Based Software Verification. - Pham Ngoc Hung; Toshiaki Aoki; Takuya Katayama (ICTAC, 2009)

Detecting and Analyzing State Inconsistencies in Multi-task Software. - Toshiaki Aoki; Tadashi Sekiguchi; Masayuki Hirayama; Tomoji Kishi (ISORC, 2009)

An effective framework for assume-guarantee verification of evolving component-based software. - Pham Ngoc Hung; Toshiaki Aoki; Takuya Katayama (EVOL/IWPSE, 2009)

Modular Conformance Testing and Assume-Guarantee Verification for Evolving Component-Based Software. - Pham Ngoc Hung; Toshiaki Aoki; Takuya Katayama (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2009)

Model checking education for software engineers in Japan. - Hideaki Nishihara; Koichi Shinozaki; Koji Hayamizu; Toshiaki Aoki; Kenji Taguchi 001; Fumihiro Kumeno (ACM SIGCSE Bull., 2009)

Evolution of a course on model checking for practical applications. - Yasuyuki Tahara; Nobukazu Yoshioka; Kenji Taguchi 001; Toshiaki Aoki; Shinichi Honiden (ACM SIGCSE Bull., 2009)

Non-regular Adaptation of Services Using Model Checking. - Hsin-Hung Lin; Toshiaki Aoki; Takuya Katayama (ISORC, 2010)

Modeling of Real-Time System Designs for Parametric Analysis. - Chaiwat Sathawornwichit; Toshiaki Aoki; Takuya Katayama (RTCSA, 2010)

Automatic Generation of Model Checking Scripts Based on Environment Modeling. - Kenro Yatake; Toshiaki Aoki (SPIN, 2010)

A Minimized Assumption Generation Method for Component-Based Software Verification. - Pham Ngoc Hung; Viet Ha Nguyen 001; Toshiaki Aoki; Takuya Katayama (IEICE Trans. Inf. Syst., 2010)

Conformance Testing for OSEK/VDX Operating System Using Model Checking. - Jiang Chen; Toshiaki Aoki (APSEC, 2011)

Automated Adaptor Generation for Services Based on Pushdown Model Checking. - Hsin-Hung Lin; Toshiaki Aoki; Takuya Katayama (ECBS, 2011)

Conformance Verification between Web Service Choreography and Implementation Using Learning and Model Checking. - Warawoot Pacharoen; Toshiaki Aoki; Athasit Surarerks; Pattarasinee Bhattarakosol (ICWS, 2011)

Model Checking of OSEK/VDX OS Design Model Based on Environment Modeling. - Kenro Yatake; Toshiaki Aoki (ICTAC, 2012)

An Improvement of Minimized Assumption Generation Method for Component-Based Software Verification. - Pham Ngoc Hung; Viet Ha Nguyen 001; Toshiaki Aoki; Takuya Katayama (RIVF, 2012)

A Variability Management Method for Software Configuration Files. - Hiroaki Tanizaki; Toshiaki Aoki; Takuya Katayama (SEKE, 2012)

Faithfully formalizing OSEK/VDX operating system specification. - Dieu-Huong Vu; Toshiaki Aoki (SoICT, 2012)

On Optimization of Minimized Assumption Generation Method for Component-Based Software Verification. - Pham Ngoc Hung; Viet Ha Nguyen 001; Toshiaki Aoki; Takuya Katayama (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2012)

Automated Adaptor Generation for Behavioral Mismatching Services Based on Pushdown Model Checking. - Hsin-Hung Lin; Toshiaki Aoki; Takuya Katayama (IEICE Trans. Inf. Syst., 2012)

SMT-based enumeration of object graphs from UML class diagrams. - Kenro Yatake; Toshiaki Aoki (ACM SIGSOFT Softw. Eng. Notes, 2012)

A Practical Study of Debugging Using Model Checking. - Hideto Ogawa; Makoto Ichii; Fumihiko Kumeno; Toshiaki Aoki (APSEC (2), 2013)

Preserving Correctness of Requirements Evolution through Refinement in Event-B. - Kriangkrai Traichaiyaporn; Toshiaki Aoki (APSEC (1), 2013)

SMT-Based Bounded Model Checking for OSEK/VDX Applications. - Haitao Zhang; Toshiaki Aoki; Hsin-Hung Lin; Min Zhang 002; Yuki Chiba; Kenro Yatake (APSEC (1), 2013)

Building a Body of Knowledge on Model Checking for Software Development. - Kenji Taguchi 001; Hideaki Nishihara; Toshiaki Aoki; Fumihiro Kumeno; Koji Hayamizu; Koichi Shinozaki (COMPSAC, 2013)

An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol. - Xiaoyun Guo; Hsin-Hung Lin; Kenro Yatake; Toshiaki Aoki (FTSCS, 2013)

Refinement Tree and Its Patterns: A Graphical Approach for Event-B Modeling. - Kriangkrai Traichaiyaporn; Toshiaki Aoki (FTSCS, 2013)

Towards Formal Description of Standards for Automotive Operating Systems. - Hirokazu Yatsu; Takahiro Ando; Weiqiang Kong; Kenji Hisazumi; Akira Fukuda; Toshiaki Aoki; Kokichi Futatsugi (ICST Workshops, 2013)

An Approach for Checking OSEK/VDX Applications. - Haitao Zhang; Toshiaki Aoki; Kenro Yatake; Min Zhang 002; Hsin-Hung Lin (QSIC, 2013)

Evaluation of Operational Vulnerability in Cloud Service Management Using Model Checking. - Shinji Kikuchi; Toshiaki Aoki (SOSE, 2013)

Checking the Conformance of a Promela Design to its Formal Specification in Event-B. - Dieu-Huong Vu; Yuki Chiba; Kenro Yatake; Toshiaki Aoki (FTSCS, 2014)

A Spin-Based Approach for Checking OSEK/VDX Applications. - Haitao Zhang; Toshiaki Aoki; Yuki Chiba (FTSCS, 2014)

Experimental Fault Analysis Process Implemented Using Model Extraction and Model Checking. - Hideto Ogawa; Makoto Ichii; Fumihiro Kumeno; Toshiaki Aoki (COMPSAC, 2015)

Modeling Safety Requirements of ISO26262 Using Goal Trees and Patterns. - Toshiaki Aoki; Kriangkrai Traichaiyaporn; Yuki Chiba; Masahiro Matsubara; Masataka Nishi; Fumio Narisawa (FTSCS, 2015)

Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications. - Haitao Zhang; Toshiaki Aoki; Yuki Chiba (ICST, 2015)

A Framework for Verifying the Conformance of Design to Its Formal Specifications. - Dieu-Huong Vu; Yuki Chiba; Kenro Yatake; Toshiaki Aoki (IEICE Trans. Inf. Syst., 2015)

Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach. - Haitao Zhang; Toshiaki Aoki; Yuki Chiba (IEICE Trans. Inf. Syst., 2015)

Verifying OSEK/VDX OS Design Using Its Formal Specification. - Dieu-Huong Vu; Yuki Chiba; Kenro Yatake; Toshiaki Aoki (TASE, 2016)

A spiral process of formalization and verification: A case study on verification of the scheduling mechanism of OSEK/VDX. - Min Zhang 002; Toshiaki Aoki; Yueying He (J. Inf. Secur. Appl., 2016)

A Reusable Framework for Modeling and Verifying In-Vehicle Networking Systems in the Presence of CAN and FlexRay. - Xiaoyun Guo; Hsin-Hung Lin; Toshiaki Aoki; Yuki Chiba (APSEC, 2017)

Domain-Specific Language Facilitates Scheduling in Model Checking. - Nhat-Hoa Tran; Yuki Chiba; Toshiaki Aoki (APSEC, 2017)

Template-Based Monte-Carlo Test Generation for Simulink Models. - Takashi Tomita; Daisuke Ishii; Toru Murakami; Shigeki Takeuchi; Toshiaki Aoki (CyPhy, 2017)

Assembly program verification for multiprocessors with relaxed memory model using SMT solver. - Pattaravut Maleehuan; Yuki Chiba; Toshiaki Aoki (TASE, 2017)

Multiple Conformance to Hybrid Automata for Checking Smart House Temperature Change. - Zhengguo Yang; Toshiaki Aoki; Yasuo Tan (DS-RT, 2018)

Modeling the Required Indoor Temperature Change by Hybrid Automata for Detecting Thermal Problems. - Zhengguo Yang; Toshiaki Aoki; Yasuo Tan (PRDC, 2018)

Qualitative and quantitative analysis with scheduling policies in model checking. - Nhat-Hoa Tran; Yuki Chiba; Toshiaki Aoki (SAC, 2018)

Formalization and Verification of AUTOSAR OS Standard's Memory Protection. - Khanh Trinh Le; Yuki Chiba; Toshiaki Aoki (TASE, 2018)

A Verification Framework for Assembly Programs Under Relaxed Memory Model Using SMT Solver. - Pattaravut Maleehuan; Yuki Chiba; Toshiaki Aoki (IEICE Trans. Inf. Syst., 2018)

Integrating Static Program Analysis Tools for Verifying Cautions of Microcontroller. - Thuy Nguyen; Toshiaki Aoki; Takashi Tomita; Junpei Endo (APSEC, 2019)

Multiple Program Analysis Techniques Enable Precise Check for SEI CERT C Coding Standard. - Thu-Trang Nguyen; Toshiaki Aoki; Takashi Tomita; Iori Yamada (APSEC, 2019)

Reducing false positives of static analysis for SEI CERT C coding standard. - Thu Trang Nguyen; Pattaravut Maleehuan; Toshiaki Aoki; Takashi Tomita; Iori Yamada (CESSER-IP@ICSE, 2019)

A scalable Monte-Carlo test-case generation tool for large and complex simulink models. - Takashi Tomita; Daisuke Ishii; Toru Murakami; Shigeki Takeuchi; Toshiaki Aoki (MiSE@ICSE, 2019)

Conformance Testing of Schedulers for DSL-based Model Checking. - Nhat-Hoa Tran; Toshiaki Aoki (SPIN, 2019)

Foreword. - Toshiaki Aoki (IEICE Trans. Inf. Syst., 2019)

Model Checking in the Presence of Schedulers Using a Domain-Specific Language for Scheduling Policies. - Nhat-Hoa Tran; Yuki Chiba; Toshiaki Aoki (IEICE Trans. Inf. Syst., 2019)

Frequency Probabilistic Risk Assessment Using Coloured Petri Nets for Telemedicine. - Kenji Fujita; Kunihiko Hiraishi; Toshiaki Aoki (IEEM, 2020)

Dataset Fault Tree Analysis for Systematic Evaluation of Machine Learning Systems. - Toshiaki Aoki; Daisuke Kawakami; Nobuo Chida; Takashi Tomita (PRDC, 2020)

Comprehensive Robustness Evaluation of File Systems with Model Checking. - Jingcheng Yuan; Toshiaki Aoki; Xiaoyun Guo (QRS, 2020)

Template-Based Monte-Carlo Test-Suite Generation for Large and Complex Simulink Models. - Takashi Tomita; Daisuke Ishii; Toru Murakami; Shigeki Takeuchi; Toshiaki Aoki (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2020)

Model checking of in-vehicle networking systems with CAN and FlexRay. - Xiaoyun Guo; Toshiaki Aoki; Hsin-Hung Lin (J. Syst. Softw., 2020)

A framework for assume-guarantee regression verification of evolving software. - Hoang-Viet Tran; Pham Ngoc Hung; Viet-Ha Nguyen 001; Toshiaki Aoki (Sci. Comput. Program., 2020)

SSpinJa: Facilitating Schedulers in Model Checking. - Nhat-Hoa Tran; Toshiaki Aoki (QRS, 2021)

Compositional Test Generation of Industrial Synchronous Systems. - Daisuke Ishii; Takashi Tomita; Kenji Onishi; Toshiaki Aoki (CoRR, 2021)

Integrating pattern matching and abstract interpretation for verifying cautions of microcontrollers. - Thuy Nguyen; Takashi Tomita; Junpei Endo; Toshiaki Aoki (Softw. Test. Verification Reliab., 2021)

A Formal Specification Language Based on Positional Relationship Between Objects in Automated Driving Systems. - Kento Tanaka; Toshiaki Aoki; Tatsuji Kawai; Takashi Tomita; Daisuke Kawakami; Nobuo Chida (COMPSAC, 2022)

SMT-Based Model Checking of Industrial Simulink Models. - Daisuke Ishii; Takashi Tomita; Toshiaki Aoki; The Quyen Ngo; Thi Bich Ngoc Do; Hideaki Takai (ICFEM, 2022)

Analysis and Enhancement of Self-sovereign Identity System Properties Compiling Standards and Regulations. - Charnon Pattiyanon; Toshiaki Aoki (ICISSP, 2022)

A Method for Detecting Common Weaknesses in Self-Sovereign Identity Systems Using Domain-Specific Models and Knowledge Graph. - Charnon Pattiyanon; Toshiaki Aoki; Daisuke Ishii (MODELSWARD, 2022)

Approximate Translation from Floating-Point to Real-Interval Arithmetic. - Daisuke Ishii; Takashi Tomita; Toshiaki Aoki (NFM, 2022)

Coverage Testing of Industrial Simulink Models using Monte-Carlo and SMT-Based Methods. - Daisuke Ishii; Takashi Tomita; Toshiaki Aoki; The Quyen Ngo; Thi Bich Ngoc Do; Hideaki Takai (QRS, 2022)

Leveraging hardware-dependent knowledge extraction with multiple program analysis techniques. - Thuy Nguyen; Takashi Tomita; Junpei Endo; Geon-ung Kang; Toshiaki Aoki (SAC, 2022)

Compliance SSI System Property Set to Laws, Regulations, and Technical Standards. - Charnon Pattiyanon; Toshiaki Aoki (IEEE Access, 2022)

Selected papers from the 14th international symposium on Theoretical Aspects of Software Engineering. - Toshiaki Aoki; Qin Li 002 (Sci. Comput. Program., 2022)

Comprehensive evaluation of file systems robustness with SPIN model checking. - Jingcheng Yuan; Toshiaki Aoki; Xiaoyun Guo (Softw. Test. Verification Reliab., 2022)

Compaction of Spacecraft Operational Models with Metamodeling Domain Knowledge. - Kazunori Someya; Toshiaki Aoki; Naoki Ishihama (ENASE, 2023)

Specification Based Testing of Object Detection for Automated Driving Systems via BBSL. - Kento Tanaka; Toshiaki Aoki; Tatsuji Kawai; Takashi Tomita; Daisuke Kawakami; Nobuo Chida (ENASE, 2023)

Attack Tree Analysis for Adversarial Evasion Attacks. - Yuki Yamaguchi; Toshiaki Aoki (PRDC, 2023)

Model-Checking in the Loop Model-Based Testing for Automotive Operating Systems. - Toshiaki Aoki; Aritoshi Hata; Kazusato Kanamori; Satoshi Tanaka; Yuta Kawamoto; Yasuhiro Tanase; Masumi Imai; Fumiya Shigemitsu; Masaki Gondo; Tomoji Kishi (CoRR, 2023)

Bridging Gaps between Scenario-Based Safety Analysis and Simulation-based Testing for Autonomous Driving Systems. - Phaiboon Jaradnaparatana; Buntita Sriarunothai; Chutikarn Kamsem; Supithcha Jongphoemwatthanaphon; Burit Sihabut; Duong Dinh Tran; Toshiaki Aoki (PRDC, 2024)

Generating Critical Scenarios for Testing Automated Driving Systems. - Trung-Hieu Nguyen; Truong-Giang Vuong; Hong-Nam Duong; Son Nguyen; Hieu Dinh Vo; Toshiaki Aoki; Thu-Trang Nguyen (CoRR, 2024)

Performance Evaluation of Multi-Head Logging in Flash File Systems. - Jingcheng Yuan; Kiyofumi Tanaka; Toshiaki Aoki (COMPSAC, 2025)

Modeling Language for Scenario Development of Autonomous Driving Systems. - Toshiaki Aoki; Takashi Tomita; Tatsuji Kawai; Daisuke Kawakami; Nobuo Chida (FormaliSE, 2025)

A Reasoning and Explicit Algebraic Theory for BBSL in Event-B: EB4BBSL Framework. - Peter Riviere; Duong Dinh Tran; Takashi Tomita; Toshiaki Aoki (ABZ, 2025)

Enhancing Decision-Making Safety in Autonomous Driving Through Online Model Checking. - Duong Dinh Tran; Akira Hasegawa; Peter Riviere; Takashi Tomita; Toshiaki Aoki (ABZ, 2025)

Specification-Based Testing of the Image-Recognition Performance of Automated Driving Systems. - Kento Tanaka; Toshiaki Aoki; Takashi Tomita; Daisuke Kawakami; Nobuo Chida (IEEE Access, 2025)

A Case Study on Model Checking and Runtime Verification for Awkernel. - Akira Hasegawa; Ryuta Kambe; Toshiaki Aoki; Yuuki Takano (CoRR, 2025)