An Approach to Automated Runtime Verification for Timed Systems: Applications to Web Services

摘要

Software testing plays an important role in verifying and assessing the quality of a software application. There are various testing approaches proposed for different application scenarios. In this paper, we propose a new passive testing approach to verifying a timed trace with respect to a set of constraints. With the extension of Nomad language, we are able to formally describe all constraints and combine conditions by logical operations AND and OR into expressions. By well organizing and evaluating the expressions, we are able to carry out runtime verification message by message in a timed trace. In addition to the theoretical framework, we have also developed a software tool known as RV4WS (Runtime Verification for Web Services) for the automation of our testing approach, and implemented all algorithms in the paper with this tool. We conduct a case study of web service composition to verify the effectiveness of our approach and tool.