Enhanced Version of ETI (Electronic Tool Integration) Platform

Organisation:	Universities of Potsdam and Dortmund (GERMANY)
Functionality:	Interactive experimentation with and service based coordination of heterogeneous tools.
Tools used:	HLL (High Level Language) METAFrame jABC
Period:	2007
Description:	Already 10 years ago, the Electronic Tool Integration (ETI) platform associated to Springer's STTT Journal offered an online portal that provided interactive experimentation with and service-based coordination of heterogeneous tools. In today's terminology, it turns out that ETI provided a model-driven, service-oriented platform for the user-side orchestration of complex services (in the ETI application domain, complex verification processes that used heterogeneous algorithms and mediators provening from different verification toolsets). In particular, ETI offered the following features: Automatic, declarative service discovery based on ontologies (implemented as multifaceted taxonomies accessible and browsable via a hypertext system); Model based, graphical service orchestration, analogous to modern BPEL editors (based on an own executable orchestration language called HLL); An execution engine for the orchestrated services (based on an HLL interpreter); Formal verification of the complex services via model checking; Automatic synthesis of sequential orchestrations and of (data or functionality) mediators via a synthesis algorithm for a semantic variant of LTL. The current work revisits the five above contributions of ETI by using as running example the orchestration of CADP activities as ETI services. CADP was used at the time ETI was launched to illustrate an ETI user session, and the functionalities are still valid today, given that "the CADP toolsuite evolved and matured over the past decade to become a reference environment for the verification of distributed processes." CADP is one of the tools that are being integrated in the new, Web service-based jETI environment that constitutes the technical platform for the jETI-FMICS community. The FMICS-jETI platform, developed within the Verified Software Repository (VSR) Grand Challenge, is a collaborative demonstrator based on the jETI technology. It provides as repository a collection of verification tools and facilities to orchestrate them in a remote and simple way.
Conclusions:	The automatic tool composition feature of ETI based on LTL synthesis allows to produce all (shortest/minimal) solutions, with the intent to provide the end-user with maximum insight into the potential design space. Future work on ETI includes the investigation of other forms of synthesis approaches (e.g., game-based) in order to reveal their application profiles, and the enhancement of the user-friendliness in terms of graphical support for specifications.
Publications:	[Margaria-Steffen-07] Tiziana Margaria and Bernhard Steffen. "LTL Guided Planning: Revisiting Automatic Tool Composition in ETI". In Proceedings of the 31st IEEE/NASA Software Engineering Workshop SEW'2007 (Columbia, USA), IEEE Computer Society Press, pp. 214-226, March 2007. Full version available from the CADP Web site in PDF or PostScript
Contact:	Technische Universität Dortmund Fakultät für Informatik Lehrstuhl für Programmiersysteme Otto-Hahn-Str. 14 44227 Dortmund Germany Tel: (0231) 755-5800 Fax: (0231) 755-5802 Email: [email protected]
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page