Presentation 2012-01-26
A Study for Bounded Model Checking of UML State Machines Using SMT Solvers
Hayato NIIMURA, Toshiyuki MIYAMOTO,
PDF Download Page PDF download Page Link
Abstract(in Japanese) (See Japanese page)
Abstract(in English) Recently, SAT-based bounded model checking has received attention as an efficient symbolic model checking technique. It is known that for model checking of distributed systems with data SMT solvers is more effective than SAT solvers. We have proposed cbUML as a subset of UML to design and verify systems based on SOA. In this paper, we study a bounded model checking technique using SMT solvers to verify state machines of cbUML.
Keyword(in Japanese) (See Japanese page)
Keyword(in English) SOA / UML / state machine diagram / synchronous and asynchronous / bounded model checking
Paper # MSS2011-58,SS2011-43
Date of Issue

Conference Information
Committee MSS
Conference Date 2012/1/19(1days)
Place (in Japanese) (See Japanese page)
Place (in English)
Topics (in Japanese) (See Japanese page)
Topics (in English)
Chair
Vice Chair
Secretary
Assistant

Paper Information
Registration To Mathematical Systems Science and its applications(MSS)
Language JPN
Title (in Japanese) (See Japanese page)
Sub Title (in Japanese) (See Japanese page)
Title (in English) A Study for Bounded Model Checking of UML State Machines Using SMT Solvers
Sub Title (in English)
Keyword(1) SOA
Keyword(2) UML
Keyword(3) state machine diagram
Keyword(4) synchronous and asynchronous
Keyword(5) bounded model checking
1st Author's Name Hayato NIIMURA
1st Author's Affiliation Graduate School of Engineering, Osaka University()
2nd Author's Name Toshiyuki MIYAMOTO
2nd Author's Affiliation Graduate School of Engineering, Osaka University
Date 2012-01-26
Paper # MSS2011-58,SS2011-43
Volume (vol) vol.111
Number (no) 405
Page pp.pp.-
#Pages 6
Date of Issue