|
2014-01-01
A paper titled Improved
device driver reliability through hardware verification
reuse has been accepted for publication in the
16th
ASPLOS Conference. The paper is the result of a
collaboration with Intel (Hillsboro, OR) lead by SSRG
researcher Leonid Ryzhyk.
|
|
A further 150K external funding was approved for
AURIN/HTS project to integrate HTS data on the national
map
|
|
2013-12-17: Seminar Bourke (INRIA & ENS - Paris) on
Mechanization of a mesh network routing protocol & the
proof of its loop freedom in Isabelle/HOL
|
|
This talk describes recently completed work to transfer a
formal but pencil-and-paper model and analysis of a
wireless mesh network protocol (AODV) into the proof
assistant Isabelle/HOL. The nodes of such networks are
reactive systems that cooperate to provide a global
service (the sending of messages from node to node)
satisfying certain correctness properties (messages are
never sent in circles).
|
|
2013-12-09: Seminar Khakpour (Royal Institute of Technology
KTH - Stockholm) on Formal Verification of Information Flow
Security for a Simple ARM-Based Separation Kernel
|
|
A separation kernel simulates a distributed environment
using a single physical machine by executing partitions
in isolation and appropriately controlling communication
among them. We present a formal verification of
information security for a simple separation kernel for
ARMv7.
|
|
2013-11-12: Seminar Schryen (University of Regensburg) on
Emergency Response in Natural Disaster Management
|
|
Emergency Response in Natural Disaster Management:
Allocation and Scheduling of Rescue Units Natural
disasters, such as earthquakes, tsunamis and hurricanes,
cause tremendous harm each year. In order to reduce
casualties and economic losses during the response phase,
rescue units must be allocated and scheduled efficiently.
As this problem is one of the key issues in emergency
response and has been addressed only rarely in
literature, we suggest a decision support model that
minimises the sum of completion times of incidents
weighted by their severity.
|
|
2013-11-01: Seminar Kopetz (Technical University of Vienna)
on The Time-Triggered Architecture
|
|
The Time-Triggered Architecture (TTA) provides a
computing infrastructure for the design and
implementation of dependable distributed embedded
systems. A large real-time application is decomposed into
nearly autonomous clusters and nodes, and a
fault-tolerant global time base of known precision is
generated at every node. In the TTA, this global time is
used to precisely specify the interfaces among the nodes,
to simplify the communication and agreement protocols, to
perform prompt error detection, and to guarantee the
timeliness of real- time applications.
|
