SeSFJava: A Framework for Design and Assertion-Testing Of Concurrent Systems

Abstract

Many elegant formalisms have been developed for specifying and reasoning about concurrent systems. However, these formalisms have not been widely used by developers and programmers of concurrent systems. One reason is that most formal methods involve techniques and tools not familiar to programmers, for example, a specification language very different from C, C++ or Java. SeSF is a framework for design, verification and testing of concurrent systems that attempts to address these concerns by keeping the theory close to the programmer's world. SeSF considers "layered compositionality". Here, a composite system consists of layers of component systems, and "services" define the allowed sequences of interactions between layers. SeSF uses conventional programming languages to define services. Specifically, SeSF is a markup language that can be integrated with any programming language. We have integrated SeSF into Java, resulting in what we call SeSFJava. We developed a testing harness for SeSFJava, called SeSFJava Harness, in which a (distributed) SeSFJava program can be executed, and the execution checked against its service and any other correctness assertion. A key capability of the SeSFJava Harness is that one can test the final implementation of a concurrent system, rather than just an abstract representation of it. We have two major applications of SeSFJava and the Harness. The first is to the TCP transport layer, where service specification is cast in SeSFJava and the system is tested under SeSFJava Harness. The second is to a Gnutella network. We define the intended services of Gnutella -- which was not done before to the best of our knowledge -- and we tested an open-source implementation, namely Furi, against the service.