Extending the applicability of the neko framework for the validation and verification of distributed algorithms

In this paper we present our recent work extending the applicability of a toolset for the fast prototyping, verification and quantitative validation of dependable distributed systems and algorithms. Neko is a framework and a communication platform that allows rapid prototyping of distributed algorithms; the same implementation of an algorithm can be exercised both on top of real and simulated networks, allowing simulative and experimental qualitative and, using the NekoStat extension, quantitative analyses. The core of the Neko framework is written in Java (J2SE), being thus highly portable; however it requires the translation into Java of existing algorithms, written in other languages, that one wants to analyze. The Neko package contains also utilities that help users to configure campaigns of experiments; these supports are really useful, but they are made as Perl scripts and Unix C code and are thus directly usable only on Unix systems. Our work aimed at extending the applicability of the tool was made towards two directions. On one side we included in the framework the utilities to allow a direct integration of existing C/C++ algorithms in Neko applications, avoiding the translation into Java that may be error prone and that may also fail in correctly represent some low level details of the algorithms. Since most of the running distributed algorithms are written in C/C++, allowing a direct analysis of C/C++ existing legacy distributed algorithms, we widely extend the applicability of Neko and improve the faithfulness of analy ses performed. The paper describes the extensions made and illustrates the use of the tool on an algorithm whose Java translation does not have the original behavior. On the other side, we made a pure Java code (J2SE, Java 2 Standard Edi tion) porting of all utilities helping Neko users in the definition of simul ative/experimental campaigns, obtaining thus a complete J2SE version of Neko