Trustworthy Systems

CAmkES glue code semantics

Authors

Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz

NICTA

UNSW

Abstract

This document describes the formal dynamic semantics of CAmkES glue code, in particular of the communication stubs generated for components at compile time. The semantics is based on a simple concurrent imperative language with message passing that is easy to extend and instantiate for specific applications. Instead of one generic semantics for all systems, we take the approach of generating a high-level semantic description for each specific ADL component specification to ease verification of specific systems in the future.

We show the definitions and types for expressing components and glue code, and provide some examples of generated Isabelle theories with synchronous, asynchronous, and shared memory communication.

BibTeX Entry

  @techreport{Fernandez_GAKK_13:tr,
    address          = {Australia},
    author           = {Fernandez, Matthew and Gammie, Peter and Andronick, June and Klein, Gerwin and Kuz, Ihor},
    institution      = {NICTA and UNSW},
    issn             = {1833-9646-7633},
    keywords         = {camkes, sel4, idl, glue code},
    month            = nov,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7633.pdf},
    title            = {{CAmkES} Glue Code Semantics},
    year             = {2013}
  }

Download