Chocolat/SMV: A Translator from CafeOBJ into SMV

Chocolat/SMV is a translator that takes a CafeOBJ specification of a transition system called an OTS and generates an SMV specification of a finite version of the OTS. The primary purpose of the translation is to find errors lurked in CafeOBJ specifications of OTSs with SMV.

• Type: Conference
• Year: 2005
• Where: PDCAT
• Authors: Kazuhiro Ogata, Masahiro Nakano, Masaki Nakamura, Kokichi Futatsugi
• Keywords: Cafeobj Specifications, Distributed And Parallel Computing, PDCAT 2005, SMV Specification, finite Version