The Specification and Implementation of a Model of Computation

Abstract

Separating a complex software system into individual components with well-defined interfaces is a common practice in software engineering intended to simplify reasoning about the system. Establishing a precise set of rules that define components and how they interact over the interfaces is necessary in order to formulate expectations about the possible behaviors that can arise from their composition. These rules are commonly called a Model of Computation (MoC); they establish the legal syntactical, structural, behavioral, and temporal patterns over which components execute. Various approaches have been developed to define MoC-s and their influence over system behavior. The work presented here describes a new approach for specifying MoC-s operationally within a formal modeling framework that captures both event-triggered and time-triggered behaviors. Equipped with this new reasoning framework, an illustrative example is provided to show how a common MoC for real-time systems can be implemented on physical hardware and off-the-shelf software. By first modeling the MoC, the execution logic that orchestrates components is established without introducing limitations of the physical system. Following the realization of the implementation, the model can be updated to reflect these limitations in order to give developers a more realistic view of how a MoC influences system behavior in a realistic deployment setting.