Formal Passive Testing of Service-Oriented Systems

This paper presents a formal framework to perform passive testing of service-oriented systems. Our approach uses the historical interaction files between web services to check the absence of faults. It uses a set of properties, that we call invariants, to represent the most relevant expected behaviour of the web services under test. Intuitively, an invariant expresses the fact that each time the system under test performs a given sequence of actions, it must exhibit a behavior reflected in the invariant. Invariants can be defined from a local point of view, that is, to check properties of isolated web services, and from a global point of view, that is, to check web service interaction properties. In order to increase applicability and adaption to a real environment, we assume that we do not have a global log. We show how to use local logs (recorded in each web service) in order to check local properties and how to combine them in order to check global properties.