オブジェクト指向開発では，一般に，分析工程において複数の視点から対象システムのモデル化を行う．データフローは，ソフトウェア分析において重要な視点であり，いわゆる，「ソフトウェア開発の三種の神器」の1つとして知られている．そのデータフローの視点は，最近のオブジェクト指向開発において益々重要になりつつある．そこで，本論文では，オブジェクト指向分析モデルにおけるデータフローの特徴づけを行い，モデル検査技術を用いたデータフロー解析手法を提案する．