Oberseminar 20.10.2015
14:15h - 15:45h
Raum 115, Oet. 67
-------------------------------------------------------
Tu Quang Tran - Behavioral Guarantees in a Voluntary Peer-to-Peer Cloud System
Bachelorarbeit, betreut von Prof. Dr. Rolf Hennicker und Annabelle Klarl
The Science Cloud Platform is one of the three case studies investigated in the ASCENS project, which describes the software systems which form a cloud providing a platform for application execution. In the cloud, individual nodes take part in teams, contribute a part of their computing power and communicate with other nodes to deploy, store and execute the user-defined applications. The Science Cloud Platform was modeled with HELENA, in which by adopting roles, individual nodes participate in task-oriented teams called ensembles and performs role-specific behaviors for collaboration with other nodes. This thesis presents the examination of the HELENA model of the Science Cloud Platform against its goals. In the first step, we define five achieve goals and two maintain goals of this platform and specify them with the linear temporal logic formulas. In the second step, we implement the HELENA model with the domain specific language HELENA-Text and use the executable PROMELA specifications translated by code generator to check this model against the goals determined in the first step. To perform the model checking we use the program SPIN and two methods for program compilation in SPIN, which are exhaustive search and bit state space search. Our results provide the number of reached states and created processes, the used memory, the elapsed time and discussions about them.
-------------------------------------------------------
Joschka Rinke (Mitarbeiter PST) - Generating a time-dependent network based on trajectory data
The growth of population in large cities turns them into metropolises and is
creating massive infrastructural problems as the road networks of those cities
are not designed to deal with such a traffic load. Those cities suddenly have to
deal with a lot more traffic on their roads, which results in massive traffic jams
especially at peak times. The consequences are highly increased trip times and
a high polution.
A lot of works provide fast routing techniques in static road networks and
in recent years some fast routing algorithms that work in time-dependent networks, like time-dependent SHARC routing, have been developed, too.
But so far time-dependent road networks on which those algorithms work and
that are not simulated hardly exist.
The goal of this work is to introduce a time-dependent graph network
based on trajectory data. When using a time-dependent network the trip
time between a start and an end point depends on the point of time at which
the trip is started. The route of choice gets calculated depending on the
weekday and the time of the day. Thereby the actual trip time can be reduced
significantly compared to static algorithms by avoiding highly frequented roads
during certain times of a day. Furthermore the use of a time-dependent routing
algorithm based on a real world trajectory data network might even rectify the
traffic on commonly used roads and improve the environmental situation.
To generate such a network the T-Drive data set which was partly made
public in 2011 by Microsoft Research was used. The excerpt used for this work
consists of 10.357 GPS log les of taxis covering a total distance of 9 million
kilometers in the metropole region of Beijing, China. The logged GPS data
was mapped to an extract of the OSM graph and information regarding the
drive through times was extracted and integrated in the graph system.
For the extraction of the time-dependent information and the integration
into the graph network the existing MARiO framework was expanded. MARiO
is an open source framework providing algorithms and mathematical functions
for multi attribute routing in Open Street Map and is easy to expand.
The final result is an exemplary way of extracting time-dependent information
from trajectory data and integrating that information into an OSM
graph which then can be used for time-dependent routing.
