Modeling of component environment in presence of callbacks and autonomous activities

Abstract

A popular approach to compositional verification of component-based applications is based on the assume-guarantee paradigm, where an assumption models behavior of an environment for each component. Real-life component applications often involve complex interaction patterns like callbacks and autonomous activities, which have to be considered by the model of environment’s behavior. In general, such patterns can be properly modeled only by a formalism that (i) supports independent atomic events for method invocation and return from a method and (ii) allows to specify explicit interleaving of events on component’s provided and required interfaces - the formalism of behavior protocols satisfies these requirements. This paper attempts to answer the question whether the model involving only events on provided interfaces (calling protocol) could be valid under certain constraints on component behavior. The key contribution are the constraints on interleaving of events related to callbacks and autonomous activities, which are expressed via syntactical patterns, and evaluation of the proposed constraints on real-life component applications.