Networking course projects are usually described by an informal specification and a collection of test cases. Students often misunderstand the specification or oversimplify it to fit just the test cases. Using formal methods eliminates these misunderstandings and allows the students to test their projects thoroughly, but at the expense of learning a new language. SeSF (Services and Systems Framework) is one way to overcome this obstacle. In SeSF, both implementations and services are defined by programs in conventional languages, thereby, eliminating the need to teach the students a new language. SeSF is a markup language that can be integrated with any conventional language. The integration of SeSF and Java is called SeSFJava. SeSFJava provides a technique to mechanically test whether student projects conform to their corresponding specifications, thereby, providing the instructors with a technique for semi-automated grading.We present a four-phase transport protocol project, and describe how SeSFJava is used in specifying, testing and grading the different phases of this project. The use of SeSF significantly (1) increased the percentage of students who completed the projects, (2) reduced their email queries about the specification, and (3) reduced the grading time.

Many formal specification languages and associated tools have been developed for network protocols. Ultimately, formal language specifications have to be compiled into a conventional programming language and this involves manual intervention (even with automated tools). This manual work is often error prone because the programmer is not familiar with the formal language. So our goal is to verify and test the ultimate implementation of a network protocol, rather than an abstract representation of it. We present a framework, called services and systems framework (SeSF), in which implementations and services are defined by programs in conventional languages, and mechanically tested against each other. SeSF is a markup language that can be integrated with any conventional language. We integrate SeSF into Java, resulting in what we call SeSFJava. We present a service-and-assertion checking harness for SeSFJava, called SeSFJava harness, in which distributed SeSFJava programs can be executed, and the execution checked against services and any other correctness assertions. The harness can test the final implementation of a concurrent system. We present an application to a data transfer service and sliding window protocol implementation. SeSFJava and the harness has been used in networking courses to specify and test transmission control protocol-like transport protocols and service.