Leveraging Software Architectures to Guide and Verify the Development of Sense/Compute/Control Applications

TL;DR

This paper introduces a behavioral contract approach within software architectures to better specify, generate support, and verify interactions in Sense/Compute/Control applications, bridging abstract and concrete specifications.

Contribution

It proposes a new notion of behavioral contracts for architecture descriptions, enabling improved implementation guidance and verification for Sense/Compute/Control systems.

Findings

Behavioral contracts effectively specify allowed component interactions.

The approach supports code generation and static verification.

Application to Sense/Compute/Control architectures demonstrates practical benefits.

Abstract

A software architecture describes the structure of a computing system by specifying software components and their interactions. Mapping a software architecture to an implementation is a well known challenge. A key element of this mapping is the architecture's description of the data and control-flow interactions between components. The characterization of these interactions can be rather abstract or very concrete, providing more or less implementation guidance, programming support, and static verification. In this paper, we explore one point in the design space between abstract and concrete component interaction specifications. We introduce a notion of behavioral contract that expresses the set of allowed interactions between components, describing both data and control-flow constraints. This declaration is part of the architecture description, allows generation of extensive programming support, and enables various verifications. We instantiate our approach in an architecture description language for the domain of Sense/Compute/Control applications, and describe associated compilation and verification strategies.