概要説明 CPS(Cyber-Physical Systems)型の組込みシステムは制御対象プラントと制御ソフトウェアが複雑に関係することから、設計物の整合性確認が難しいという問題がある。本研究では、ダイアグラムに基づく記法SysMLで表現されたモデリング記述から数値制約を抽出し、制約系の整合性を自動検査する方法を考察した。特に、自動検査エンジンとして Yices を用いて実験を行うことで提案方式を確認した。この研究によって、茨城大学上田研究室の修士学生加藤氏がESS2010優秀論文賞を受賞した。 詳細説明 組込みシステムの高機能化、大規模・複雑化に対応することが必要になり、開発上流工程でのモデリングが重要になってきている。IT系ソフトウェアで使われているUML系のダイアグラムに基づく記法を、組込みシステム開発でも利用するという目的から、SysML等が提案された。SysMLはUMLを拡張し