Virtual stationary timed automata for mobile networks
Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2009. === Includes bibliographical references (p. 339-347). === In this thesis, we formally define a programming abstraction for mobile networks called the Virtual Stationary Automata progra...
Main Author: | |
---|---|
Other Authors: | |
Format: | Others |
Language: | English |
Published: |
Massachusetts Institute of Technology
2009
|
Subjects: | |
Online Access: | http://hdl.handle.net/1721.1/47745 |
id |
ndltd-MIT-oai-dspace.mit.edu-1721.1-47745 |
---|---|
record_format |
oai_dc |
spelling |
ndltd-MIT-oai-dspace.mit.edu-1721.1-477452019-05-02T15:57:35Z Virtual stationary timed automata for mobile networks Nolte, Tina Ann, 1979- Nancy Lynch. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Electrical Engineering and Computer Science. Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2009. Includes bibliographical references (p. 339-347). 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. by Tina Ann Nolte. Ph.D. 2009-10-01T15:37:41Z 2009-10-01T15:37:41Z 2009 2009 Thesis http://hdl.handle.net/1721.1/47745 428735461 eng 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. http://dspace.mit.edu/handle/1721.1/7582 347 p. application/pdf Massachusetts Institute of Technology |
collection |
NDLTD |
language |
English |
format |
Others
|
sources |
NDLTD |
topic |
Electrical Engineering and Computer Science. |
spellingShingle |
Electrical Engineering and Computer Science. Nolte, Tina Ann, 1979- Virtual stationary timed automata for mobile networks |
description |
Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2009. === Includes bibliographical references (p. 339-347). === 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. === by Tina Ann Nolte. === Ph.D. |
author2 |
Nancy Lynch. |
author_facet |
Nancy Lynch. Nolte, Tina Ann, 1979- |
author |
Nolte, Tina Ann, 1979- |
author_sort |
Nolte, Tina Ann, 1979- |
title |
Virtual stationary timed automata for mobile networks |
title_short |
Virtual stationary timed automata for mobile networks |
title_full |
Virtual stationary timed automata for mobile networks |
title_fullStr |
Virtual stationary timed automata for mobile networks |
title_full_unstemmed |
Virtual stationary timed automata for mobile networks |
title_sort |
virtual stationary timed automata for mobile networks |
publisher |
Massachusetts Institute of Technology |
publishDate |
2009 |
url |
http://hdl.handle.net/1721.1/47745 |
work_keys_str_mv |
AT noltetinaann1979 virtualstationarytimedautomataformobilenetworks |
_version_ |
1719031900267347968 |