Connecting Remote Tools: Do it by yourSELF!
by María Alpuente and Salvador Lucas
Fifty years of research in computer science have seen a huge number of programming languages, theories, techniques, and program analysis tools come into existence. The World-Wide Web makes it possible to gain access to resources in a number of ways, ranging from remote downloads followed by local executions, to remote execution via WWW services. Unfortunately however, few of the existing systems and tools are effectively connectable, even if they address similar problems or rely on similar theoretical bases.
As recently noticed by T. Hoare, the quest for a verifying compiler is a classic, but still urgent problem for both the software industry and the computer science community. Of course, program verification, debugging and analysis (especially when oriented towards improving program efficiency) will be essential components of such a tool. Moreover, the effective development of such a system will require an incremental and cooperative effort from work teams all around the world. Thanks to the Internet, the physical distance separating those teams is becoming less and less important. Unfortunately, many existing systems and tools are not really suitable for working together, even if they address closely related problems or rely on similar theoretical bases. The Internet and middleware technology, however, provide numerous possibilities for removing integration barriers and dramatically improving the reusability of previous theoretical results and development efforts.
We can further motivate this point of view with two concrete examples extracted from our personal experience: model checking and termination analysis. Model checking is becoming a standard technique for automated software verification. Its success has made the term relatively popular for describing other verification methods. An example is the automatic analysis of general correctness properties of concurrent systems that do not require a particular representation with a property language (eg deadlock absence, dead code and arithmetic errors). Moreover, advances in model checking position it as an important contributor in the future development of the verifying compiler.
Still, model checking is not commonly used in, for example, object-oriented 'programming, where 'de facto standard modelling methods (eg UML) and programming languages (eg C, C++ and Java) are common practice. The current pattern in verification tools for these languages essentially consists of automatic model extraction from the source code to the input language of existing, efficient model-checking tools like SPIN. However, the use of these tools for verifying parts of a program currently being developed in, say, Java is not easy. First, the syntax of Java programs does not correspond to the input language of any of the above-mentioned tools (eg Promela). Some translation is therefore required, but hardly covers a subset of the language. Second, there is no easy way of calling one of these tools from the Java interpreter. Third, we lack methods to analyse the results, especially counter-examples for non-deterministic executions. This is partly due to the different interfaces of the tools. For instance, in contrast to the usual GUI of most Java interpreters, SPIN has a command-based interface accepting text from the standard input (stdin), and writes its results on the standard output (stdout). Fourth, the tools can be written in different programming languages, which may make the eventual embedding of one tool into another significantly more difficult. Finally, there is no documented API to gain external access to the functionalities of the applications.
As a different (although related) motivating example, we consider the termination analysis of programs written in programming languages such as CafeOBJ, Elan, Erlang, Maude and OBJ, whose operational principle is based on reducing expressions according to the well-known paradigm of term rewriting. Proofs of termination of term-rewriting systems can be used to prove termination of such programs. A number of termination tools exist which can, in fact, be used to address this problem: for instance, the tool MU-TERM can be used to prove termination of simple Maude programs (see Figure). Termination of rewriting has also recently been related to certain classes of standard verification problems that can be reduced to termination problems.
Unfortunately, however, it is not easy to connect independently developed analysis tools (like MU-TERM) to a practical environment such as the Maude interpreter. The problems are analogous to those enumerated above.
Interoperability (ie making it possible for a program on one system to access programs and data on another system) is a general problem in software engineering, and a number of solutions (namely, middleware systems) have been devised to solve it. The developers of (formal) software tools should consider such solutions to be an essential part of their design and development. Tackling this problem seriously would also be a positive step for the research community in formal methods and declarative languages. These areas are often used (or should be used) to design and implement analysis tools. By isolating the various aspects of a complex tool (eg GUI, numeric computation, constraint solving, program transformation and manipulation etc) into different modules possibly written in different languages, we gain the flexibility to use the most appropriate language. Tightly coupled support techniques such as RPC, CORBA and COM have not undergone sufficient experimentation and development in this setting. The XML WWW services (or just WWW services) also provide a flexible architecture for achieving interoperability of loosely coupled systems that are developed in different programming languages. Again, few efforts have been made to conciliate the design and development of software tools with this technology. We claim that, when considering the design and use of software systems and analysis tools, not only correctness and efficiency must be systematically considered but also interoperability across platforms, applications and programming languages.
Starting this year, we plan to develop these ideas into the research project SELF (Software Engineering and Lightweight Formalisms). This will include research on:
- Suitable XML-like formats for expressing the most important features of currently used (families of) programming languages. A related effort has been recently addressed for developing the CLI/CTS/CLS/CLR framework, which forms the basis of Microsoft's .NET platform.
- Suitable XML sub-languages for expressing analysis/verification requirements to existing tools.
- Middleware translators and interfaces from existing programming languages to the formalisms or lower-level languages which underlie the program analysis tools.
- The inclusion of existing verification and analysis tools into the SOAP/WSDL/UDDI framework of XML WWW services in order to gain systematic access to their functionality.
Links:
SELF: http://self.lcc.uma.es/
ELP group: http://www.dsic.upv.es/users/elp/elp.html
Please contact:
Salvador Lucas, Universidad Politécnica de Valencia/SparCIM
E-mail: slucas
dsic.upv.es
http://www.dsic.upv.es/~slucas
