Keyword : model checking


Timed Model-Based Formal Analysis of a Scheduler of Qplus-AIR, an ARINC-653 Compliance RTOS
Sanghyun YOON Dong-Ah LEE Eunji PAK Taeho KIM Junbeom YOO 
Publication:   
Publication Date: 2017/10/01
Vol. E100-D  No. 10 ; pp. 2644-2647
Type of Manuscript:  LETTER
Category: Software System
Keyword: 
Qplus-AIRmodel checkingreal-time operating systemsafety
 Summary | Full Text:PDF(446.6KB)

Model Checking of Embedded Assembly Program Based on Simulation
Satoshi YAMANE Ryosuke KONOSHITA Tomonori KATO 
Publication:   
Publication Date: 2017/08/01
Vol. E100-D  No. 8 ; pp. 1819-1826
Type of Manuscript:  PAPER
Category: Software Engineering
Keyword: 
embedded assembly programmodel checkingsimulation
 Summary | Full Text:PDF(346.8KB)

Verifying Scenarios of Proximity-Based Federations among Smart Objects through Model Checking and Its Advantages
Reona MINODA Shin-ichi MINATO 
Publication:   
Publication Date: 2017/06/01
Vol. E100-D  No. 6 ; pp. 1172-1181
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Formal techniques
Keyword: 
ubiquitous computingcatalytic reaction networkformal verificationmodel checkingsmart object
 Summary | Full Text:PDF(1.5MB)

State Number Calculation Problem of Workflow Nets
Mohd Anuaruddin BIN AHMADON Shingo YAMAGUCHI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2015/06/01
Vol. E98-D  No. 6 ; pp. 1128-1136
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Petri net
Keyword: 
Petri netstate number calculation problemprocess treesolvabilitycomputational complexitymodel checking
 Summary | Full Text:PDF(1.1MB)

A Model-Checking Approach for Fault Analysis Based on Configurable Model Extraction
Hideto OGAWA Makoto ICHII Tomoyuki MYOJIN Masaki CHIKAHISA Yuichiro NAKAGAWA 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2015/06/01
Vol. E98-D  No. 6 ; pp. 1150-1160
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Model Checking
Keyword: 
model checkingfault analysismodel transformation
 Summary | Full Text:PDF(1.3MB)

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)

A Formal Verification of a Subset of Information-Based Access Control Based on Extended Weighted Pushdown System
Pablo LAMILLA ALVAREZ Yoshiaki TAKATA 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2014/05/01
Vol. E97-D  No. 5 ; pp. 1149-1159
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Formal Verification
Keyword: 
weighted pushdown systemsaccess controlmodel checking
 Summary | Full Text:PDF(886.3KB)

Verifying Business Rules Using Model-Checking Techniques for Non-specialist in Model-Checking
Yoshitaka AOKI Saeko MATSUURA 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2014/05/01
Vol. E97-D  No. 5 ; pp. 1097-1108
Type of Manuscript:  Special Section PAPER (Special Section on Knowledge-Based Software Engineering)
Category: 
Keyword: 
model checkingUPPAALEclipse
 Summary | Full Text:PDF(2.6MB)

Automated Route Planning for Milk-Run Transport Logistics with the NuSMV Model Checker
Takashi KITAMURA Keishi OKAMOTO 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2013/12/01
Vol. E96-D  No. 12 ; pp. 2555-2564
Type of Manuscript:  Special Section PAPER (Special Section on Parallel and Distributed Computing and Networking)
Category: 
Keyword: 
automated route planningtransport logisticsmodel checking
 Summary | Full Text:PDF(474.2KB)

Model Checking an OSEK/VDX-Based Operating System for Automobile Safety Analysis
Yunja CHOI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2013/03/01
Vol. E96-D  No. 3 ; pp. 735-738
Type of Manuscript:  LETTER
Category: Dependable Computing
Keyword: 
OSEK/VDXTrampolinemodel checkingsafety analysis
 Summary | Full Text:PDF(582.5KB)

Synthesis and Refinement Check of Sequence Diagrams
Hisashi MIYAZAKI Tomoyuki YOKOGAWA Sousuke AMASAKI Kazuma ASADA Yoichiro SATO 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2012/09/01
Vol. E95-D  No. 9 ; pp. 2193-2201
Type of Manuscript:  Special Section PAPER (Special Section on Software Reliability Engineering)
Category: 
Keyword: 
UMLsequence diagramrefinementmodel checkingLTSA
 Summary | Full Text:PDF(530.5KB)

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)

An Efficient Translation Method from Timed Petri Nets to Timed Automata
Shota NAKANO Shingo YAMAGUCHI 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2012/08/01
Vol. E95-A  No. 8 ; pp. 1402-1411
Type of Manuscript:  PAPER
Category: Concurrent Systems
Keyword: 
timed Petri netstimed automatathe amount of descriptionmodel checkingsignaling pathway
 Summary | Full Text:PDF(1.1MB)

On-the-Fly Trace Generation Approach to the Security Analysis of the TMN Protocol with Homomorphic Property: A Petri Nets-Based Method
Yongyuth PERMPOONTANALARP Apichai CHANGKHANAK 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2012/01/01
Vol. E95-D  No. 1 ; pp. 215-229
Type of Manuscript:  PAPER
Category: Dependable Computing
Keyword: 
formal methods for cryptographic protocolsmodel checkingPetri nets
 Summary | Full Text:PDF(589.3KB)

Checking On-the-Fly Universality and Inclusion Problems of Visibly Pushdown Automata
Nguyen VAN TANG Hitoshi OHSAKI 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2011/12/01
Vol. E94-A  No. 12 ; pp. 2794-2801
Type of Manuscript:  Special Section PAPER (Special Section on Mathematical Systems Science and its Applications)
Category: 
Keyword: 
verification of infinite state systemsvisibly pushdown automatainclusion and universalitymodel checkingP-automata
 Summary | Full Text:PDF(879KB)

Modeling, Verification and Testing of Web Applications Using Model Checker
Kei HOMMA Satoru IZUMI Kaoru TAKAHASHI Atsushi TOGASHI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2011/05/01
Vol. E94-D  No. 5 ; pp. 989-999
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Software Development Methodology
Keyword: 
Web applicationmodelingtestingautomatamodel checkingSpin
 Summary | Full Text:PDF(523.7KB)

Probabilistic Symmetry Reduction for a System with Ring Buffer
Toshifusa SEKIZAWA Takashi TOYOSHIMA Koichi TAKAHASHI Kazuko TAKAHASHI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2011/05/01
Vol. E94-D  No. 5 ; pp. 967-975
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: System Analysis
Keyword: 
probabilistic symmetry reductionring buffermodel checkingthe Ising modelAIS
 Summary | Full Text:PDF(308.3KB)

QoS Analysis of Real-Time Distributed Systems Based on Hybrid Analysis of Probabilistic Model Checking Technique and Simulation
Takeshi NAGAOKA Akihiko ITO Kozo OKANO Shinji KUSUMOTO 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2011/05/01
Vol. E94-D  No. 5 ; pp. 958-966
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Model Checking
Keyword: 
QoSprobabilistic automatonsimulationmodel checking
 Summary | Full Text:PDF(2.2MB)

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)

An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop
Takeshi NAGAOKA Kozo OKANO Shinji KUSUMOTO 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2010/05/01
Vol. E93-D  No. 5 ; pp. 994-1005
Type of Manuscript:  Special Section PAPER (Special Section on Formal Approach)
Category: Model Checking
Keyword: 
model checkingtimed automatonmodel abstractionCEGAR
 Summary | Full Text:PDF(1.5MB)

Model Checking of Real-Time Properties of Resource-Bound Process Algebra
Junkil PARK Jungjae LEE Jin-Young CHOI Insup LEE 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2009/11/01
Vol. E92-A  No. 11 ; pp. 2781-2789
Type of Manuscript:  Special Section PAPER (Special Section on Theory of Concurrent Systems and its Applications)
Category: 
Keyword: 
ACSRmodel checkingaction-based modelingreal-time temporal logicresource-bound process algebra
 Summary | Full Text:PDF(369.1KB)

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)

A Model Checking Method of Soundness for Workflow Nets
Munenori YAMAGUCHI Shingo YAMAGUCHI Minoru TANAKA 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2009/11/01
Vol. E92-A  No. 11 ; pp. 2723-2731
Type of Manuscript:  Special Section PAPER (Special Section on Theory of Concurrent Systems and its Applications)
Category: 
Keyword: 
model checkingtemporal logicworkflow netsasymmetric choiceWoflan
 Summary | Full Text:PDF(461.1KB)

Query Language for Location-Based Services: A Model Checking Approach
Christian HOAREAU Ichiro SATOH 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2008/04/01
Vol. E91-D  No. 4 ; pp. 976-985
Type of Manuscript:  Special Section PAPER (Special Section on Knowledge-Based Software Engineering)
Category: Ubiquitous Computing
Keyword: 
ubiquitous computinglocation-based servicesquery languagemodel checking
 Summary | Full Text:PDF(481.3KB)

Coverage Estimation Using Transition Perturbation for Symbolic Model Checking in Hardware Verification
Xingwen XU Shinji KIMURA Kazunari HORIKAWA Takehiko TSUCHIYA 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2006/12/01
Vol. E89-A  No. 12 ; pp. 3451-3457
Type of Manuscript:  Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
Category: Simulation and Verification
Keyword: 
model checkingtransition coverage
 Summary | Full Text:PDF(414.2KB)

Swiss Cheese Test Case Generation for Web Services Testing
Wei-Tek TSAI Xiao WEI Yinong CHEN Ray PAUL Bingnan XIAO 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2005/12/01
Vol. E88-D  No. 12 ; pp. 2691-2698
Type of Manuscript:  Special Section PAPER (IEICE/IEEE Joint Special Section on Autonomous Decentralized Systems)
Category: 
Keyword: 
Web servicesWeb services testingtest case generationvulnerabilitymodel checking
 Summary | Full Text:PDF(963KB)

Policy Controlled System and Its Model Checking
Shigeta KUNINOBU Yoshiaki TAKATA Naoya NITTA Hiroyuki SEKI 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2005/07/01
Vol. E88-D  No. 7 ; pp. 1685-1696
Type of Manuscript:  PAPER
Category: Application Information Security
Keyword: 
policy controlpolicy controlled systemverificationmodel checkingpushdown system
 Summary | Full Text:PDF(1.3MB)

Model Checking of RADIUS Protocol in Wireless Networks
Il-Gon KIM Jin-Young CHOI 
Publication:   IEICE TRANSACTIONS on Communications
Publication Date: 2005/01/01
Vol. E88-B  No. 1 ; pp. 397-398
Type of Manuscript:  LETTER
Category: Internet
Keyword: 
model checkingCasperCSPFDRRADIUS
 Summary | Full Text:PDF(53.6KB)

Verification of a Microcomputer Program Specification Embedded in a Reactive System
Yasunori ISHIHARA Kiichiro NINOMIYA Hiroyuki SEKI Daisuke TAKAHARA Yutaka YAMADA Shigesada OMOTO 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 2000/05/25
Vol. E83-D  No. 5 ; pp. 1082-1091
Type of Manuscript:  PAPER
Category: Software Engineering
Keyword: 
compositional verificationmodel checkingreactive systemreachability graph
 Summary | Full Text:PDF(806.3KB)

CTL Model Checking of Time Petri Nets Using Geometric Regions
Tomohiro YONEDA Hikaru RYUBA 
Publication:   IEICE TRANSACTIONS on Information and Systems
Publication Date: 1998/03/25
Vol. E81-D  No. 3 ; pp. 297-306
Type of Manuscript:  PAPER
Category: Fault Tolerant Computing
Keyword: 
CTLmodel checkingtime Petri netsgeometric regionformal verification
 Summary | Full Text:PDF(880.7KB)

Formal Design Verification of Sequential Machines Based on Symbolic Model Checking for Branching Time Regular Temporal Logic
Kiyoharu HAMAGUCHI Hiromi HIRAISHI Shuzo YAJIMA 
Publication:   IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 1992/10/25
Vol. E75-A  No. 10 ; pp. 1220-1229
Type of Manuscript:  Special Section PAPER (Special Section on VLSI Design and CAD Algorithms)
Category: 
Keyword: 
design verificationsequential machinestemporal logicmodel checkingbinary decision diagram
 Summary | Full Text:PDF(786KB)