Abstract
Recently, the temporal constraint satisfiability is regarded as an important criterion in Web service composition to guarantee its timely completion. This leads to a new challenge in analyzing the compatibility of Web services under temporal constraints. The existing methods either do not consider message mismatches between services in a composition or suffer from state-space explosion by verifying a service composition model as a whole; or lack the ability to generate execution paths of each participating service. In this paper, we present a Petri net-based method to address these three issues in a holistic manner, and also in a modular way. Compared with the existing work, the proposed approach not only composes Web services by adding a mediation net to deal with message mismatches, but also checks the compatibility w.r.t. temporal constraints by generating modular timed state graphs. Furthermore, the reliable and usable execution paths that satisfy the timed compatibility can be derived to guide service execution and avoid any temporal exception.