Fault localization in service compositions

Abstract

Service-oriented architectures aim at the assemblance of service compositions out of independent, small services. In a model-based design, such service compositions first of all exist as formal models, describing the employed services with their interfaces plus their assemblance. Such formal models allow for an early analysis with respect to user requirements. While a large number of such analysis methods exist today, this is less so for techniques localizing faults in erroneous service compositions. In this paper, we extend an existing technique for fault localization in software to the model-based domain. The approach employs maximum satisfiability solving (MAX-SAT) of trace formulae encoding faulty program runs. Contrary to software, we can, however, not use testing as a way of determining such faulty runs, but instead employ SMT solving. Moreover, due to the usage of undefined function symbols encoding concepts of domain ontologies, the trace formula also needs an encoding of the logical structure producing the fault. We furthermore show how to use weights on soft constraints in the MAX-SAT instance to steer the solver to particular types of faults.