Database of Case Studies Achieved Using CADP

Formal Verification of ToolBus Scripts

Organisation: CWI, Vrije Universiteit, Universiteit van Amsterdam, and Technische Universiteit Eindhoven (The Netherlands)

Method: Tscript
mCRL2

Tools used: CADP (Construction and Analysis of Distributed Processes)
mCRL2

Domain: Coordination.

Period: 2008

Size: n/a

Description: ToolBus provides a simple, service-oriented view on how to organize software systems by separating the coordination of software components from the actual computation that they perform. ToolBus organizes a system along the lines of a programmable software bus. A system is programmed using the scripting language Tscript, based on the process algebra ACP (Algebra of Communicating Processes) and abstract data types. The tools connected to the ToolBus can be written in any language and can run on different machines.

A Tscript program 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 achieve this, a Tscript program is first translated into a mCRL2 specification, from which the labeled transition system (LTS) is generated. Then, correctness properties are checked on this LTS using either mCRL2 or CADP. This approach has been applied on a standard example from the ToolBus distribution: a distributed auction system.

Conclusions: The general aim of this work is to have a process algebra-based software development environment where both formal verification and production of an executable system is possible. The translation scheme from Tscript to mCRL2 makes it possible to apply formal verification techniques to Tscript, and thus to check behavioral properties of large software systems that have been built with the ToolBus.

Publications: [Fokkink-Klint-Lisser-Usenko-08] Wan Fokkink, Paul Klint, Bert Lisser and Yaroslav S. Usenko. "Towards Formal Verification of ToolBus Scripts". Proceedings of the 12th international conference on Algebraic Methodology and Software Technology, pp.160-166, Springer-Verlag, July 2008.
Available on-line at: http://www.cs.vu.nl/~wanf/pubs/amast08.pdf
or from our FTP site in PDF or PostScript

[Fokkink-Klint-Lisser-Usenko-10] Wan Fokkink, Paul Klint, Bert Lisser and Yaroslav S. Usenko. "Automated Translation and Analysis of a ToolBus Script for Auctions". Lecture Notes in Computer Science, Fundamentals of Software Engineering, pages 308-323, Springer-Verlag, 2010, Volume 5961.
Available on line at: http://www.springerlink.com/content/9040068v35248m84/
or from our FTP site in PDF or PostScript
Contact:
Wan Fokkink
Vrije Universiteit Amsterdam
Department of Computer Science
Section Theoretical Computer Science
De Boelelaan 1081a
1081 HV Amsterdam
The Netherlands
Tel: +31 20 598 7735
Fax: +31 20 598 7653
Email: wanf@cs.vu.nl



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page