株式会社デンソーが長崎県立大学との自動車関連の研究プロジェクトでAdaCore社SPARKを採用「Freedom from Interference」を実証するためにフォーマルメソッドを適用