default search action
Toshiaki Aoki
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2023
- [c66]Kazunori Someya, Toshiaki Aoki, Naoki Ishihama:
Compaction of Spacecraft Operational Models with Metamodeling Domain Knowledge. ENASE 2023: 102-113 - [c65]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: 250-261 - [c64]Yuki Yamaguchi, Toshiaki Aoki:
Attack Tree Analysis for Adversarial Evasion Attacks. PRDC 2023: 46-52 - [i5]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 abs/2310.00973 (2023) - [i4]Yuki Yamaguchi, Toshiaki Aoki:
Attack Tree Analysis for Adversarial Evasion Attacks. CoRR abs/2312.16957 (2023) - 2022
- [j21]Charnon Pattiyanon, Toshiaki Aoki:
Compliance SSI System Property Set to Laws, Regulations, and Technical Standards. IEEE Access 10: 99370-99393 (2022) - [j20]Toshiaki Aoki, Qin Li:
Selected papers from the 14th international symposium on Theoretical Aspects of Software Engineering. Sci. Comput. Program. 219: 102821 (2022) - [j19]Jingcheng Yuan, Toshiaki Aoki, Xiaoyun Guo:
Comprehensive evaluation of file systems robustness with SPIN model checking. Softw. Test. Verification Reliab. 32(6) (2022) - [c63]Kento Tanaka, Toshiaki Aoki, Tatsuji Kawai, Takashi Tomita, Daisuke Kawakami, Nobuo Chida:
A Formal Specification Language Based on Positional Relationship Between Objects in Automated Driving Systems. COMPSAC 2022: 950-955 - [c62]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: 156-172 - [c61]Charnon Pattiyanon, Toshiaki Aoki:
Analysis and Enhancement of Self-sovereign Identity System Properties Compiling Standards and Regulations. ICISSP 2022: 133-144 - [c60]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: 219-226 - [c59]Daisuke Ishii, Takashi Tomita, Toshiaki Aoki:
Approximate Translation from Floating-Point to Real-Interval Arithmetic. NFM 2022: 733-751 - [c58]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: 422-433 - [c57]Thuy Nguyen, Takashi Tomita, Junpei Endo, Geon-ung Kang, Toshiaki Aoki:
Leveraging hardware-dependent knowledge extraction with multiple program analysis techniques. SAC 2022: 1827-1836 - [i3]Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai:
SMT-Based Model Checking of Industrial Simulink Models. CoRR abs/2206.02992 (2022) - 2021
- [j18]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) - [c56]Nhat-Hoa Tran, Toshiaki Aoki:
SSpinJa: Facilitating Schedulers in Model Checking. QRS 2021: 632-641 - [i2]Daisuke Ishii, Takashi Tomita, Toshiaki Aoki:
Approximate Translation from Floating-Point to Real-Interval Arithmetic. CoRR abs/2112.02804 (2021) - [i1]Daisuke Ishii, Takashi Tomita, Kenji Onishi, Toshiaki Aoki:
Compositional Test Generation of Industrial Synchronous Systems. CoRR abs/2112.05411 (2021) - 2020
- [j17]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. 103-A(2): 451-461 (2020) - [j16]Xiaoyun Guo, Toshiaki Aoki, Hsin-Hung Lin:
Model checking of in-vehicle networking systems with CAN and FlexRay. J. Syst. Softw. 161 (2020) - [j15]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: 102439 (2020) - [c55]Kenji Fujita, Kunihiko Hiraishi, Toshiaki Aoki:
Frequency Probabilistic Risk Assessment Using Coloured Petri Nets for Telemedicine. IEEM 2020: 1098-1102 - [c54]Toshiaki Aoki, Daisuke Kawakami, Nobuo Chida, Takashi Tomita:
Dataset Fault Tree Analysis for Systematic Evaluation of Machine Learning Systems. PRDC 2020: 100-109 - [c53]Jingcheng Yuan, Toshiaki Aoki, Xiaoyun Guo:
Comprehensive Robustness Evaluation of File Systems with Model Checking. QRS 2020: 99-110 - [e2]Toshiaki Aoki, Qin Li:
International Symposium on Theoretical Aspects of Software Engineering, TASE 2020, Hangzhou, China, December 11-13, 2020. IEEE 2020, ISBN 978-1-7281-4086-5 [contents]
2010 – 2019
- 2019
- [j14]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. 102-D(7): 1280-1295 (2019) - [j13]Toshiaki Aoki:
Foreword. IEICE Trans. Inf. Syst. 102-D(8): 1438 (2019) - [c52]Thu-Trang Nguyen, Toshiaki Aoki, Takashi Tomita, Iori Yamada:
Multiple Program Analysis Techniques Enable Precise Check for SEI CERT C Coding Standard. APSEC 2019: 70-77 - [c51]Thuy Nguyen, Toshiaki Aoki, Takashi Tomita, Junpei Endo:
Integrating Static Program Analysis Tools for Verifying Cautions of Microcontroller. APSEC 2019: 86-93 - [c50]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: 39-46 - [c49]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: 41-48 - [c48]Nhat-Hoa Tran, Toshiaki Aoki:
Conformance Testing of Schedulers for DSL-based Model Checking. SPIN 2019: 208-225 - 2018
- [j12]Pattaravut Maleehuan, Yuki Chiba, Toshiaki Aoki:
A Verification Framework for Assembly Programs Under Relaxed Memory Model Using SMT Solver. IEICE Trans. Inf. Syst. 101-D(12): 3038-3058 (2018) - [c47]Zhengguo Yang, Toshiaki Aoki, Yasuo Tan:
Multiple Conformance to Hybrid Automata for Checking Smart House Temperature Change. DS-RT 2018: 224-233 - [c46]Zhengguo Yang, Toshiaki Aoki, Yasuo Tan:
Modeling the Required Indoor Temperature Change by Hybrid Automata for Detecting Thermal Problems. PRDC 2018: 135-144 - [c45]Nhat-Hoa Tran, Yuki Chiba, Toshiaki Aoki:
Qualitative and quantitative analysis with scheduling policies in model checking. SAC 2018: 1873-1880 - [c44]Khanh Trinh Le, Yuki Chiba, Toshiaki Aoki:
Formalization and Verification of AUTOSAR OS Standard's Memory Protection. TASE 2018: 68-75 - 2017
- [c43]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: 140-149 - [c42]Nhat-Hoa Tran, Yuki Chiba, Toshiaki Aoki:
Domain-Specific Language Facilitates Scheduling in Model Checking. APSEC 2017: 417-426 - [c41]Takashi Tomita, Daisuke Ishii, Toru Murakami, Shigeki Takeuchi, Toshiaki Aoki:
Template-Based Monte-Carlo Test Generation for Simulink Models. CyPhy 2017: 63-78 - [c40]Pattaravut Maleehuan, Yuki Chiba, Toshiaki Aoki:
Assembly program verification for multiprocessors with relaxed memory model using SMT solver. TASE 2017: 1-8 - 2016
- [j11]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: 41-53 (2016) - [c39]Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, Toshiaki Aoki:
Verifying OSEK/VDX OS Design Using Its Formal Specification. TASE 2016: 81-88 - 2015
- [j10]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. 98-D(6): 1137-1149 (2015) - [j9]Haitao Zhang, Toshiaki Aoki, Yuki Chiba:
Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach. IEICE Trans. Inf. Syst. 98-D(10): 1765-1776 (2015) - [c38]Hideto Ogawa, Makoto Ichii, Fumihiro Kumeno, Toshiaki Aoki:
Experimental Fault Analysis Process Implemented Using Model Extraction and Model Checking. COMPSAC 2015: 95-104 - [c37]Toshiaki Aoki, Kriangkrai Traichaiyaporn, Yuki Chiba, Masahiro Matsubara, Masataka Nishi, Fumio Narisawa:
Modeling Safety Requirements of ISO26262 Using Goal Trees and Patterns. FTSCS 2015: 206-221 - [c36]Haitao Zhang, Toshiaki Aoki, Yuki Chiba:
Yes! You Can Use Your Model Checker to Verify OSEK/VDX Applications. ICST 2015: 1-10 - 2014
- [c35]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: 110-126 - [c34]Haitao Zhang, Toshiaki Aoki, Yuki Chiba:
A Spin-Based Approach for Checking OSEK/VDX Applications. FTSCS 2014: 239-255 - 2013
- [c33]Hideto Ogawa, Makoto Ichii, Fumihiko Kumeno, Toshiaki Aoki:
A Practical Study of Debugging Using Model Checking. APSEC (2) 2013: 134-139 - [c32]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: 307-314 - [c31]Kriangkrai Traichaiyaporn, Toshiaki Aoki:
Preserving Correctness of Requirements Evolution through Refinement in Event-B. APSEC (1) 2013: 315-322 - [c30]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: 784-789 - [c29]Xiaoyun Guo, Hsin-Hung Lin, Kenro Yatake, Toshiaki Aoki:
An UPPAAL Framework for Model Checking Automotive Systems with FlexRay Protocol. FTSCS 2013: 36-53 - [c28]Kriangkrai Traichaiyaporn, Toshiaki Aoki:
Refinement Tree and Its Patterns: A Graphical Approach for Event-B Modeling. FTSCS 2013: 246-261 - [c27]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: 13-14 - [c26]Haitao Zhang, Toshiaki Aoki, Kenro Yatake, Min Zhang, Hsin-Hung Lin:
An Approach for Checking OSEK/VDX Applications. QSIC 2013: 113-116 - [c25]Shinji Kikuchi, Toshiaki Aoki:
Evaluation of Operational Vulnerability in Cloud Service Management Using Model Checking. SOSE 2013: 37-48 - 2012
- [j8]Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama:
Automated Adaptor Generation for Behavioral Mismatching Services Based on Pushdown Model Checking. IEICE Trans. Inf. Syst. 95-D(7): 1882-1893 (2012) - [j7]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. 95-A(9): 1451-1460 (2012) - [j6]Kenro Yatake, Toshiaki Aoki:
SMT-based enumeration of object graphs from UML class diagrams. ACM SIGSOFT Softw. Eng. Notes 37(4): 1-8 (2012) - [c24]Kenro Yatake, Toshiaki Aoki:
Model Checking of OSEK/VDX OS Design Model Based on Environment Modeling. ICTAC 2012: 183-197 - [c23]Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama:
An Improvement of Minimized Assumption Generation Method for Component-Based Software Verification. RIVF 2012: 1-6 - [c22]Hiroaki Tanizaki, Toshiaki Aoki, Takuya Katayama:
A Variability Management Method for Software Configuration Files. SEKE 2012: 672-677 - [c21]Dieu-Huong Vu, Toshiaki Aoki:
Faithfully formalizing OSEK/VDX operating system specification. SoICT 2012: 13-20 - [e1]Toshiaki Aoki, Kenji Taguchi:
Formal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012. Proceedings. Lecture Notes in Computer Science 7635, Springer 2012, ISBN 978-3-642-34280-6 [contents] - 2011
- [c20]Jiang Chen, Toshiaki Aoki:
Conformance Testing for OSEK/VDX Operating System Using Model Checking. APSEC 2011: 274-281 - [c19]Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama:
Automated Adaptor Generation for Services Based on Pushdown Model Checking. ECBS 2011: 130-139 - [c18]Warawoot Pacharoen, Toshiaki Aoki, Athasit Surarerks, Pattarasinee Bhattarakosol:
Conformance Verification between Web Service Choreography and Implementation Using Learning and Model Checking. ICWS 2011: 722-723 - 2010
- [j5]Pham Ngoc Hung, Viet Ha Nguyen, Toshiaki Aoki, Takuya Katayama:
A Minimized Assumption Generation Method for Component-Based Software Verification. IEICE Trans. Inf. Syst. 93-D(8): 2172-2181 (2010) - [c17]Hsin-Hung Lin, Toshiaki Aoki, Takuya Katayama:
Non-regular Adaptation of Services Using Model Checking. ISORC 2010: 170-174 - [c16]Chaiwat Sathawornwichit, Toshiaki Aoki, Takuya Katayama:
Modeling of Real-Time System Designs for Parametric Analysis. RTCSA 2010: 81-91 - [c15]Kenro Yatake, Toshiaki Aoki:
Automatic Generation of Model Checking Scripts Based on Environment Modeling. SPIN 2010: 58-75
2000 – 2009
- 2009
- [j4]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. 92-A(11): 2772-2780 (2009) - [j3]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): 38-44 (2009) - [j2]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): 45-50 (2009) - [c14]Pham Ngoc Hung, Toshiaki Aoki, Takuya Katayama:
A Minimized Assumption Generation Method for Component-Based Software Verification. ICTAC 2009: 277-291 - [c13]Toshiaki Aoki, Tadashi Sekiguchi, Masayuki Hirayama, Tomoji Kishi:
Detecting and Analyzing State Inconsistencies in Multi-task Software. ISORC 2009: 326-330 - [c12]Pham Ngoc Hung, Toshiaki Aoki, Takuya Katayama:
An effective framework for assume-guarantee verification of evolving component-based software. EVOL/IWPSE 2009: 109-118 - 2008
- [c11]Toshiaki Aoki:
Model Checking Multi-Task Software on Real-Time Operating Systems. ISORC 2008: 551-555 - 2007
- [c10]Toshiaki Aoki, Takuya Katayama:
Statechart-based Verification of Object-Oriented Design Models. APSEC 2007: 278-285 - [c9]Jaejoon Lee, Isabel John, Toshiaki Aoki, John D. McGregor:
SPLC 2007 Dectoral Symposium. SPLC (2) 2007: 155-156 - 2005
- [j1]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. 88-D(6): 1105-1116 (2005) - [c8]Kenro Yatake, Toshiaki Aoki, Takuya Katayama:
Implementing Application-Specific Object-Oriented Theories in HOL. ICTAC 2005: 501-516 - [c7]Toshiaki Aoki, Takuya Katayama:
Formalization and Analysis of Dataflow in Object-Oriented Design Models. ISORC 2005: 95-105 - 2004
- [c6]Toshiaki Aoki, Takuya Katayama:
Foundations for Evolutionary Construction of State Transition Models. IWPSE 2004: 143-146 - [c5]Kenro Yatake, Toshiaki Aoki, Takuya Katayama:
Collaboration-based verification of Object-Oriented models in HOL. VVEIS 2004: 78-80 - [c4]Tomoji Kishi, Toshiaki Aoki, Shin Nakajima, Natsuko Noda, Takuya Katayama:
Project Report: High-Reliable Object-Oriented Embedded Software Design. WSTFEUS 2004: 144-148 - 2002
- [c3]Mitsutaka Okazaki, Toshiaki Aoki, Takuya Katayama:
Extracting threads from concurrent objects for the design of embedded systems. APSEC 2002: 107-116 - 2001
- [c2]Toshiaki Aoki, Takaaki Tateishi, Takuya Katayama:
An Axiomatic Formalization of UML Models. pUML 2001: 13-28
1990 – 1999
- 1998
- [c1]Toshiaki Aoki, Takuya Katayama:
Unification and Consistency Verification of Object-Oriented Analysis Models. APSEC 1998: 296-303
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from , , and to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-12 23:00 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint