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

摘要

上位設計記述においては、並列動作や同期·通信を用いて設計が記述される。本研究では、同期設計の誤りによりデッドロック等の不具合がある設計のデバッグを支援する手法を提案する。具体的には、デッドロック等の不具合の原因になっている同期設計が、どのような条件下で同期されるか（または、デッドロックとなるか）を静的に解析し、その条件を出力する。SpecCで記述された並列エレベータコントローラによる実験を通して、提案手法により出力された条件によって、並列動作するプロセス間の同期が設計者の意図通りになっているかを確認することが出来ることを確認した。