Toshiaki AOKI


Verifying OSEK/VDX Applications: A Sequentialization-Based Model Checking Approach
Haitao ZHANG Toshiaki AOKI Yuki CHIBA 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2015/10/01
Vol. E98-D  No. 10  pp. 1765-1776
Type of Manuscript:  PAPER
Category: Software System
Keyword: 
OSEK/VDX applicationsFormal Software Verificationdeterministic schedulersequentialization
 Summary | Full Text:PDF(709.8KB)

A Framework for Verifying the Conformance of Design to Its Formal Specifications
Dieu-Huong VU Yuki CHIBA Kenro YATAKE Toshiaki AOKI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2015/06/01
Vol. E98-D  No. 6  pp. 1137-1149
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Formal Verification
Keyword: 
formal specificationdesign modelformal verificationmodel checkingsimulation relation
 Summary | Full Text:PDF(1.6MB)

On Optimization of Minimized Assumption Generation Method for Component-Based Software Verification
Ngoc Hung PHAM Viet Ha NGUYEN Toshiaki AOKI Takuya KATAYAMA 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2012/09/01
Vol. E95-A  No. 9  pp. 1451-1460
Type of Manuscript:  Special Section PAPER (Special Section on Software Reliability Engineering)
Category: 
Keyword: 
model checkingassume-guarantee reasoningmodular verificationlearning algorithmminimal assumption
 Summary | Full Text:PDF(1.4MB)

Automated Adaptor Generation for Behavioral Mismatching Services Based on Pushdown Model Checking
Hsin-Hung LIN Toshiaki AOKI Takuya KATAYAMA 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2012/07/01
Vol. E95-D  No. 7  pp. 1882-1893
Type of Manuscript:  PAPER
Category: Data Engineering, Web Information Systems
Keyword: 
service adaptationbehavior mismatchpushdown model checkingunbounded messages
 Summary | Full Text:PDF(1.5MB)

A Minimized Assumption Generation Method for Component-Based Software Verification
Ngoc Hung PHAM Viet Ha NGUYEN Toshiaki AOKI Takuya KATAYAMA 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2010/08/01
Vol. E93-D  No. 8  pp. 2172-2181
Type of Manuscript:  PAPER
Category: Software System
Keyword: 
model checkingassume-guarantee reasoningmodular verificationlearning algorithmminimal assumption
 Summary | Full Text:PDF(319.8KB)

Modular Conformance Testing and Assume-Guarantee Verification for Evolving Component-Based Software
Ngoc Hung PHAM Toshiaki AOKI Takuya KATAYAMA 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2009/11/01
Vol. E92-A  No. 11  pp. 2772-2780
Type of Manuscript:  Special Section PAPER (Special Section on Theory of Concurrent Systems and its Applications)
Category: 
Keyword: 
model checkingassume-guarantee reasoningmodular verificationcomponent evolutionconformance testing
 Summary | Full Text:PDF(718.7KB)

Highly Reliable Embedded Software Development Using Advanced Software Technologies
Takuya KATAYAMA Tatsuo NAKAJIMA Taiichi YUASA Tomoji KISHI Shin NAKAJIMA Shuichi OIKAWA Masahiro YASUGI Toshiaki AOKI Mitsutaka OKAZAKI Seiji UMATANI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2005/06/01
Vol. E88-D  No. 6  pp. 1105-1116
Type of Manuscript:  INVITED PAPER (Special Section on Software Engineering for Embedded Systems)
Category: 
Keyword: 
embedded softwaredesign verification operating systemreal-time garbage collection
 Summary | Full Text:PDF(1.2MB)