Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Tech Talk: Back-to-back talks on Haskell and Embedded Systems</h1> <div class='date'><time class="dtstart dt-start" title="2011-08-16T10:30:00" datetime="2011-08-16T10:30:00">Tuesday, August 16, 2011 from 10:30</time>–<time class="dtend dt-end" title="2011-08-16T11:30:00" datetime="2011-08-16T11:30:00">11:30am</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202390439'><span class='fn org p-name'>Galois, Inc</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">421 SW 6th Ave. Suite 300</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">OR</span> <span class="postal-code p-postal-code">97204</span> <div class="country-name p-country-name">US</div> (<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <p>Presented by Sebastian Niller and Nis N. Wegmann</p> <h1>1</h1> <p>title: Translation of Functionally Embedded Domain-specific Languages With Static Type Preservation by using Witnesses</p> <p>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.</p> <p>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.</p> <h1>2</h1> <p>title: From High-Level Languages to Monitoring Fault-Tolerant Hardware: Case-Studies of Runtime Verification Using Copilot</p> <p>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.</p> <p>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.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://corp.galois.com/blog/2011/8/10/tech-talks-back-to-back-talks-on-haskell-and-embedded-system.html">Website</a></li> </ul> </div>