AVR Processors as a Platform for Language-Based Security


Interface theories combining de Alfaro and Henzinger's Interface
Automata (IA) with Larsen's Modal Transition Systems (MTS) have been
developed for specifying component-based, concurrent, reactive systems.
However, subtle differences in the semantics of IA and MTS made previous
attempts sacrifice several desired properties of the combined theories,
which leads to unintuitive results in practice. E.g., one may redefine
unwanted behaviour to not being an error, when refining a specification.
With Error-preserving Modal Interface Automata (EMIA) I developed an
interface theory that addresses all of the above-mentioned
properties at once and resolves the related practical issues. In
particular, EMIA is not an arbitrary solution to these issues, but a
principled one that is related to previous interface theories via a
Galois-insertion.