Virtual stationary timed automata for mobile networks

In this thesis, we formally define a programming abstraction for mobile networks called the Virtual Stationary Automata programming layer, consisting of real mobile clients, virtual timed I/O automata called virtual stationary automata (VSAs), and a communication service connecting VSAs and client nodes. The VSAs are located at prespecified regions that tile the plane, defining a static virtual infrastructure. We present a theory of self-stabilizing emulation and use this theory to prove correct a self-stabilizing algorithm to emulate a timed VSA using the real mobile nodes that are currently residing in the VSA's region. We also specify two important services for mobile networks: motion coordination and end-to-end routing. We split the implementation of the end-to-end routing service into three smaller pieces, consisting of geographic routing and location management services with an end-to-end routing service built on top of them. We provide stabilizing implementations of each of these services using the VSA abstraction, and provide formal correctness analyses for each implementation.

Department dc:contributor.department

Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2009

Author dc:creator

• Nolte, Tina Ann, 1979-

Advisor dc:contributor.advisor

• Nancy Lynch.

• Electrical Engineering and Computer Science.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/47745

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/47745