Theses and Dissertations from UMD

Permanent URI for this communityhttp://hdl.handle.net/1903/2

New submissions to the thesis/dissertation collections are added automatically as they are received from the Graduate School. Currently, the Graduate School deposits all theses and dissertations from a given semester after the official graduation date. This means that there may be up to a 4 month delay in the appearance of a give thesis/dissertation in DRUM

More information is available at Theses and Dissertations at University of Maryland Libraries.

Browse

Filters

20051

Settings

Author: search.filters.author.Elsharnouby, Tamer MahmoudSubject: search.filters.subject.Software Engineering

Search Results

Now showing 1 - 1 of 1
  • Thumbnail Image
    Item
    SeSFJava: A Framework for Design and Assertion-Testing Of Concurrent Systems
    (2005-08-04) Elsharnouby, Tamer Mahmoud; Shankar, A. Udaya; Computer Science; Digital Repository at the University of Maryland; University of Maryland (College Park, Md.)
    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.