システムレベル設計における並列動作の同期に関するデバッグ支援手法

摘要

There are many high-level designs contain parallel execution, synchronization, or communication, and they are often error-prone. In this work, we propose a debugging support method for designs with improper syn- chronization. We derive a safe condition by static analysis in which synchronization works properly under the target design. The experiment with an elevator controller containing parallel executions shows that we can easily check whether synchronization works as the designer intended or not, by using the derived condition.%上位設計記述においては、並列動作や同期・通信を用いて設計が記述される。本研究では、同期設の誤りによりデッドロック等の不具合がある設計のデバッグを支援する手法を提案する。具体的には、ッドロック等の不具合の原因になっている同期設計が、どのような条件下で同期されるか（または、デッドロックなるか）を静的に解析し、その条件を出力する。SpecCで記述された並列エレベータコントローラによる実験を通し、提案手法により出力された条件によって、並列動作するプロセス間の同期が設計者の意図通りになっているか確認することが出来ることを確認した。