Monitor-Based Run-Time Contract Verification of Distributed Systems

The design of large scale complex systems demands the ability to correctly specify and verify as early as possible in the design cycle the interaction of the different components to ensure that the global level requirements are satisfied. We address this issue using an approach based on the notion of contract and simulation-based verification. In particular, we extend traditional contract verification methods to target distributed systems, which require an asynchronous communication paradigm. We use a pattern-based language for requirement definition, from which we generate a set of contract monitors implemented in the Simulink framework to observe the underlying system execution and flag violating behaviors. In the paper, we discuss in particular the aspects related to handling the asynchronous interaction between components and their relation to the contract monitors. An automatic towing system case study demonstrates the approach.