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

Simple item page
dc.contributor.advisorShankar, A. Udayaen_US
dc.contributor.authorElsharnouby, Tamer Mahmouden_US
dc.contributor.departmentComputer Scienceen_US
dc.contributor.publisherDigital Repository at the University of Marylanden_US
dc.contributor.publisherUniversity of Maryland (College Park, Md.)en_US
dc.date.accessioned2005-10-11T10:41:37Z
dc.date.available2005-10-11T10:41:37Z
dc.date.issued2005-08-04en_US
dc.description.abstractMany 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.en_US
dc.format.extent955492 bytes
dc.format.mimetypeapplication/pdf
dc.identifier.urihttp://hdl.handle.net/1903/2968
dc.language.isoen_US
dc.subject.pqcontrolledComputer Scienceen_US
dc.subject.pquncontrolledFormal Methodsen_US
dc.subject.pquncontrolledSoftware Engineeringen_US
dc.subject.pquncontrolledMechainical Testingen_US
dc.subject.pquncontrolledNetwork Protocolsen_US
dc.subject.pquncontrolledPeer-to-peer Networksen_US
dc.titleSeSFJava: A Framework for Design and Assertion-Testing Of Concurrent Systemsen_US
dc.typeDissertationen_US

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
umi-umd-2761.pdf
Size:
933.1 KB
Format:
Adobe Portable Document Format
Download

Collections

UMD Theses and Dissertations
Computer Science Theses and Dissertations