Automated Translation and Analysis of a ToolBus Script for Auctions

Date Added: Nov 2009
Format: PDF

ToolBus allows to connect tools via a software bus. Programming is done using the scripting language Tscript, which is based on the process algebra ACP. In previous work, the authors presented a method for analyzing a Tscript by translating it to the process algebraic language mCRL2, and then applying model checking to verify certain behavioral properties. They have implemented a prototype based on this approach. As a case study, they have applied it on a standard example from the ToolBus distribution, distributed auction, and detected a number of behavioral irregularities in this auction Tscript.