リアルタイム並行システムに対しその振舞いが仕様を満たすか， あるいはデッドロックしないかなど動作の正しさを調べるには， 複数存在する動作系列それぞれについて検証を行う必要がある． しかしシーケンス図などを用いる従来手法では一つの動作系列しか表現できず動作検証は困難である． そこでモデルチェッキングなどの手法を利用して機械的に検証を行うため， 並行計算モデルであるπ計算を用いてシステムの動作を表現するということが考えられる．
さらにリアルタイムオブジェクト指向言語とπ計算の対応付けを行うことで， リアルタイムオブジェクト指向言語を用いて実装されるリアルタイム並行システムの動作検証を対応するπ計算による記述を用いて行うことが可能となる． 逆にリアルタイム並行システムをπ計算を用いて記述及び動作検証した後， その記述に基づきリアルタイムオブジェクト指向言語を用いて実装することもできる． これはリアルタイム並行システムの開発及び品質の向上に有利である．
リアルタイム並行システムに対するπ計算を用いた記述として， 時間制約を優先度スケジューリングにより満たし優先度継承プロトコルに基づいて動作する並行システムを， π計算に優先度環境を導入した優先度付きπ計算を用いて記述する方法を提案した． この方法を用いてリアルタイム並行システムを形式的に記述することでシステムの動作検証を機械的に行うことができる．