Intersert: Assertions on Distributed Process Interaction Sessions

Program assertions typically operate on available program state such as global and local variables. To support sophisticated assert statements such as invariants on control flow or inter-process communication patterns, developers must design and maintain supporting infrastructure. It is non-obvious how to realize this infrastructure: how to maintain the data, how to access it, how to use it in assertions, how to keep the overhead low enough for embedded systems, and how to manage assertions across a distributed system.

This work demonstrates the utility of assertions on interaction history among distributed system components and solves the challenges of efficiently maintaining interaction data while providing an expressive interface for assertions. Our toolchain enables developers to program assertions on interaction history written in regular expressions that incorporate inter-process and inter-thread behavior amongst multiple components in a distributed system. We demonstrate that the interaction tracking and property verification systems incur negligible overhead, measured with several benchmarks. This work discusses our toolchain with a real-world safety-critical embedded system.