Verification of message sequence charts via template matching

Abstract

Message sequence charts are becoming a popular low-level design tool for communication systems. When applied to systems of nontrivial size, organizing and manipulating them become a challenge. We present a methodology for specifying and verifying message sequence charts. Specification is given using templates, namely charts with only partial information about the participating events and their interrelated order. "Verification is done by a search whose aim is to match templates against charts. The result of such a search either reports that no matching chart exists, or returns examples of charts that satisfy the constraints that appear in such a template. We describe the algoritilm and an implementation.