キャッツは18日、モデル検査ツールのリーディングカンパニーであるUPPAAL International（本社：スウェーデン）と、同社のモデル検査ツール『UPPAAL』（ウパール）の販売を行うことに基本合意した。キャッツはUPPAALの販売に加え、モデル検査を行うための「モデリング導入支援サービス」を合わせて提供していく。
モデル検査とは、たとえばシステムがどんな動作をしても問題ないことを数学的に証明する手法。UPPAALは、時間記述をモデルとして記述できるため、「時間に関するモデル検査に有効」という評価を世界的に得ているツールである。
UPPAALはデンマークのオルボー大学とスウェーデンのウプサラ大学が開発した、形式手法に基づいたモデリングとモデル検査を行うツール。グラフィカルなシミュレーションによってリアルタイムシステムの妥当性検査と検証を行なえるなど、時間記述付きの状態遷移モデルを作成することによって、リアルタイム制御における不具合がないことを自動検査する機能を備えている。
UPPAAL Internationalは、モデル検査技術を専門に取扱う会社として、UPPAAL開発の中心メンバーだったワン・イー氏が2007年に設立した。
昨今の組込ソフトウェア開発は、システムの巨大化・複雑化と並行して、市場ニーズの速い変化や多様性から開発期間の短期化が進んでいる。このため製品の動作テストや品質テストが不十分になりがちで、市場投入後に不具合が発見され製品回収に至るといった問題の一因となっている。このような問題に対応するためのソフトウェア検証に関して、モデル検査手法などの形式的な検証手法が注目を集めている。
キャッツの渡辺政彦取締役副社長は「組み込みシステム開発では、予想外のタイミングで動作するなどの、タイミングに起因する不具合を防止することが重要な課題となっている。UPPAALを利用することで、タイミングに起因する不具合を検出することができる」という。
キャッツは、組み込みシステム開発用CASEツール分野で1998年以来7年連続の国内シェア首位（電子情報技術産業協会調べ）であるZIPCなどを提供しており、開発支援ツールにおいて組み込みシステムの品質・生産性向上を提唱してきた。生産性向上にモデル検査手法を取り入れれば、品質や生産性が大幅に向上するということを、組み込み分野で蓄積された経験から立証している。
