Galois is pleased to host the following back-to-back tech talks.
These talks are open to the interested public. Please join us!
speakers:
Sebastian Niller and Nis N. Wegmann
time:
16 August 2011, Tuesday, 10:30 A.M.
location:
Galois, Inc.
421 SW 6th Ave
Ste 300
Portland, OR 97204
(3rd floor of the Commonwealth building)
#1
title:
Translation of Functionally Embedded Domain-specific Languages With Static Type Preservation by using Witnesses
abstract:
Static type preservation automatically guarantees type-correctness of an embedded domain-specific language (eDSL) by tying its type system to that of the host-language. Not only does this obviate the need for a custom type checker, it also preserves type-correctness during code transformations and optimizations, and simplifies and increases the efficiency of interpreters. When implementing a translator from a source DSL with type preservation to a target DSL, the commonly chosen approach requires the incorporation of extensions in the source DSL specific to the target DSL, which, in cases where multiple back-ends are required, obfuscates the source DSL and decreases the overall modularity. We show that by using witnesses, a technique which facilitates the construction of type-level proofs, we can effectively cope with this issue and implement translators without extending the source DSL.
We have applied our approach on Copilot, a Haskell-embedded domain specific language for runtime monitoring of hard real-time distributed systems, and used it for implementing two back-ends targeting the Haskell-embedded languages Atom and SBV. Our approach restrains to the Haskell 2010 Standard except for existentially and universally quantified types.
#2
title:
From High-Level Languages to Monitoring Fault-Tolerant Hardware: Case-Studies of Runtime Verification Using Copilot
abstract:
Failures of hard real-time systems can be caused by systematic faults in software and hardware, as well as by random hardware faults, and faults due to wear out of hardware components. Even if monitoring software is proven to comply to its specification, there is no guarantee that failing underlying hardware does not affect the monitors themselves. An application of distributed Copilot monitors to a redundant airspeed measurement system is presented. We show the use of monitors enables the system to withstand benign and Byzantine hardware and software faults.
The second part of the talk presents current work using Copilot
to monitor the MAVLink protocol in flight of a sub-scale model
of an Edge 540T aircraft.
bios:
Sebastian Niller works at the National Institute of Aerospace.
His interests include high-level languages, in combination with
embedded and reconfigurable systems.
Nis N. Wegmann is an intern at the National Institute of Aerospace and
a Master’s student at the University of Copenhagen.