キャッツ、福岡に「ＣＡＴＳ組込みソフトウェア研究所」を開設
キャッツ、福岡に「ＣＡＴＳ組込みソフトウェア研究所」を開設
―モデル検査や車載組込みソフトウェアのコンサルティング拠点－
キャッツ株式会社（社長・上島康男、本社・横浜市港北区）は本日、福岡市の福岡知的クラスター研究所内に、状態遷移表を利用したモデル検査や車載組込みソフトウェアの開発コンサルティング拠点となる「ＣＡＴＳ組込みソフトウェア研究所（ＣＡＴＳ Ｅｍｂｅｄｄｅｄ Ｓｏｆｔｗａｒｅ Ｌａｂ、通称ＣＥＳＬ）所長・渡辺政彦（キャッツ副社長と兼任）」を開設しました。所在地は、福岡市早良区百道浜３－８－３３です。
ＣＡＴＳ組込みソフトウェア研究所は、システム開発の上流工程（仕様・設計）で重要な、モデルベース開発プロセス、手法の構築、モデル検査、形式検証の研究を進める部門です。
キャッツの組込み開発向けＣＡＳＥツールである「ＺＩＰＣ」などを使用して、モデルベース開発における、状態遷移経路の自動検証／状態遷移表モデル検査サービス（形式仕様）を推進します。
また、ソフトウェアの時間制約についてのモデル上での数値証明や形式検証を行う「リソース・スケジューリング」の研究を進めていく計画です。
状態遷移表は、組込みシステムの振舞いをモレやヌケ無くモデリングすることが可能で、ユーザーから高い評価を得ているキャッツの主力製品のコアである表記法です。
この状態遷移表を利用したモデル検査では、状態遷移モデルで特定の条件を満たすかどうかを検査し、数理的に証明することが可能です。
システム開発の上流工程に潜在する論理的な矛盾やバグの原因排除に効果を発揮し、従来から行われてきた人手や経験に頼る膨大な試験工数による信頼性確保の問題に対して大きな効果を発揮することが多くの事例（ＨＰ参照）で実証されています。
キャッツは２００５年６月から、九州大学と福岡知的クラスター研究所（財団法人福岡県産業・科学技術振興財団）の３者で次世代モデルベース開発における状態遷移モデル検査技術（形式手法／モデル検査技術）の共同研究を行ってきました。すでに、３者の共同成果として、自動車電子部品やデジタル家電などに組み込まれるソフトウェアの設計ミスを自動探知する「ＺＩＰＣ」ベースの状態遷移モデルの形式検証ツール「Ｇａｒａｋａｂｕ」を２００６年に発表しています。
「Ｇａｒａｋａｂｕは、プログラミングの専門家３人が６時間かけて異常が見つからなかったＴ－Ｅｎｇｉｎｅベースの行先表示板の開発時の検証作業で、１０秒間に１４個の異常を発見できるといった大きな効果が確認されています。
ＣＡＴＳ組込みソフトウェア研究所は、この共同研究をさらに推進していくとともに、組み込みシステムやソフトウェア，モバイルコンピューティングなどを研究する九州大学大学院のシステム情報科学研究院情報工学部門（福田晃教授）との連携を進めて行く計画です。
特に、車載情報端末や自動車電装品など車載機器向け組込みソフトウェアの開発コンサルティング拠点となります。
以 上－
記載の社名および製品名は各社の商標または登録商標です。