PDF

URL

BibTeX

DOI

Abstract. Internet protocols encapsulate a significant amount of state, making implementing the host software complex. In this paper, we define the Statecall Policy Language (SPL) which provides a usable middle ground between ad-hoc coding and formal reasoning. It enables programmers to embed automata in their code which can be statically model-checked using SPIN and dynamically enforced. The performance overheads are minimal, and the automata also provide higher-level debugging capabilities. We also describe some practical uses of SPL by describing the automata used in an SSH server written entirely in OCaml/SPL.

Authors. Anil Madhavapeddy

See Also. This publication was part of my Functional Internet Services project.

News Updates

Nov 2009. «» Paper on a DSL for specifying temporal protocol automata at ICFEM 2009.

Jun 2005. «» Blogged about the OpenBSD C2K5 hackathon trip in Canada.