Symbolic Discord Computation for Efficient Analysis of Message Sequence Charts

スポンサーリンク

概要

• 論文の詳細を見る

• Message sequence charts (MSCs) and high-level MSCs (HMSCs) have been standardized to model interactions of parallel processes as message exchanges. We can flexibly express parallel behaviors with MSCs, but alternatively, it is possible to put unintended orders of messages into the MSCs. This paper focuses on detection of such unintended orders as discord. We propose an encoding scheme in which the analysis of an HMSC is converted into a boolean SAT problem. Experimental results show that our approach achieves efficient analysis of HMSCs which have a large number of processes or a large size of graphs. This contributes efficient analysis of specification on complex interactions.

• 2011-08-10

著者

• Kiyoharu Hamaguchi

  Osaka University

• Masaki Nakanishi

  Yamagata University

• Yosuke Kakiuchi

  Osaka University

• Tomofumi Nakagawa

  Osaka University

• Tadaaki Tanimoto

  Renesas Electronics Corporation

関連論文

• Checker Generation of Assertions with Local Variables for Model Checking
• Approximate Model Checking Using a Subset of First-order Logic
• Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic
• Symbolic Discord Computation for Efficient Analysis of Message Sequence Charts

スポンサーリンク