A Formal Semantics for the SmartFrog Configuration Language

Paul Anderson, Herry Herry

Research output: Contribution to journalArticlepeer-review

Abstract

System configuration languages are now widely used to drive the deployment and evolution of large computing infrastructures. Most such languages are highly informal, making it difficult to reason about configurations, and introducing an important source of failure. We claim that a more rigorous approach to the development and specification of these languages will help to avoid these difficulties and bring a number of additional benefits. In order to test this claim, we present a formal semantics for the core of the SmartFrog configuration language. We demonstrate how this can be used to prove important properties such as termination of the compilation process. To show that this also contributes to the practical development of clear and correct compilers, we present three independent implementations, and verify their equivalence with each other, and with the semantics. Supported by an extended example from a real configuration scenario, we demonstrate how the process of developing the semantics has improved understanding of the language, highlighted problem areas, and suggested alternative interpretations. This leads us to advocate this approach for the future development of practical configuration languages.
Original languageEnglish
Pages (from-to)309-345
Number of pages37
JournalJournal of Network and Systems Management
Volume24
Issue number2
Early online date12 Aug 2015
DOIs
Publication statusPublished - 1 Apr 2016

Keywords

  • Configuration management
  • Configuration languages
  • Semantics
  • SmartFrog
  • System administration
  • Formal specification

Fingerprint Dive into the research topics of 'A Formal Semantics for the SmartFrog Configuration Language'. Together they form a unique fingerprint.

Cite this