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.
著者
-
Hamaguchi Kiyoharu
Osaka University
-
NAKANISHI Masaki
Yamagata University
-
Kakiuchi Yosuke
Osaka University
-
Nakagawa Tomofumi
Osaka University
-
Tanimoto Tadaaki
Renesas Electronics Corporation
関連論文
- Checker Generation of Assertions with Local Variables for Model Checking
- Bit Length Optimization of Fractional Part on Floating to Fixed Point Conversion for High-Level Synthesis(Logic and High Synthesis)(VLSI Design and CAD Algorithms)
- Look Up Table Compaction Based on Folding of Logic Functions(Special Section on VLSI Design and CAD Algorithms)
- Robust Quantum Algorithms Computing OR with ε-Biased Oracles(Quantum Computing,Foundations of Computer Science)
- Bit-Length Optimization Method for High-Level Synthesis Based on Non-linear Programming Technique(System Level Design,VLSI Design and CAD Algorithms)
- An Efficient and Effective Algorithm for Online Task Placement with I/O Communications in Partially Reconfigurable FPGAs(System Level Design,VLSI Design and CAD Algorithms)
- Quantum versus Classical Pushdown Automata in Exact Computation (特集:量子計算と量子情報)
- An efficient middle-level framework for quantum circuit simulation on multiple simulator platforms (コンピュータシステム)
- Quantum Walks on the Line with Phase Parameters
- Symbolic Discord Computation for Efficient Analysis of Message Sequence Charts
- Power Efficient Design of Arithmetic Circuits Based on Embedded Memory Blocks in FPGA
- Checker Generation of Assertions with Local Variables for Model Checking