Towards Formal Verification of ToolBus Scripts
ToolBus allows one to connect tools via a software bus. Programming is done using the scripting language Tscript , which is based on the process algebra ACP. Tscript was originally designed to enable formal verification, but this option has so far not bee
- PDF / 330,750 Bytes
- 7 Pages / 430 x 660 pts Page_size
- 63 Downloads / 212 Views
Abstract. ToolBus allows one to connect tools via a software bus. Programming is done using the scripting language Tscript, which is based on the process algebra ACP. Tscript was originally designed to enable formal verification, but this option has so far not been explored in any detail. We present a method for analyzing a Tscript by translating it to the process algebraic language mCRL2, and then applying model checking to verify behavioral properties.
1
Introduction
ToolBus [1,2] provides a simple, service-oriented view on organizing software systems by separating the coordination of software components from the actual computation that they perform. It organizes a system along the lines of a programmable software bus. Programming is done using the scripting language Tscript that is based on the process algebra ACP (Algebra of Communicating Processes) [3] and abstract data types. The tools connected to the ToolBus can be written in any language and can run on different machines. A Tscript can be tested, like any other software system, to observe whether it exhibits the desired behavior. An alternative approach for analyzing communication protocols is model checking, which constitutes an automated check of whether some behavioral property is satisfied. This can be, roughly, a safety property, which must be satisfied throughout any run of the system, or a liveness property, which should eventually be satisfied in any run of the system. To perform model checking, the communication protocol must be specified in some formal language, and the behavioral properties in some temporal logic. Strong points of model checking are that it attempts to performs an exhaustive exploration of the state space of a system, and that it can often be fully automated. As one of the main aims of Tscript, Bergstra and Klint [2] mention that it should have “a formal basis and can be formally analyzed”. The formal basis is J. Meseguer and G. Ro¸su (Eds.): AMAST 2008, LNCS 5140, pp. 160–166, 2008. © Springer-Verlag Berlin Heidelberg 2008
Towards Formal Verification of ToolBus Scripts
161
offered by the process algebra ACP, but ways to formally analyze Tscripts were lacking so far. This is partly due to a number of obstructions for an automatic translation from Tscript to ACP, which are explained below. This work was initiated by the developers of the ToolBus, who are keen to integrate model checking into the design process. This paper constitutes an important step in this direction. We have charted the most important distinctions between ACP and Tscript, and investigated how Tscript can be translated into the formal modeling language mCRL2 [4]. This language is also based on the process algebra ACP, extended with equational abstract data types [5]. Since both Tscript and mCRL2 are based on data terms and ACP, an automated translation is in principle feasible. And as a result, Tscript can then be model checked using the mCRL2 or CADP toolset [6]. This method has been applied on a standard example from the ToolBus distribution: a distributed aucti
Data Loading...
