SysMLを用いたシステム開発における制約の充足可能性検証

摘要

SysMLは，ハードウェア，ソフトウェア，人などを含めたシステムの包括的なモデリングに利用でき，システムの設計，解析，検証が可能になると期待されている．しかしながら，SysMLの要求図やパラメトリック図などを用いて設計上の各種制約を記述することはできるが，それらの制約をどのように設計に織り込み，設計結果がそれらの制約を満たすかどうかを検証する方法については明らかにされていない．そこで，本稿ではFMEAを用いて要求図で表現できる抽象的な制約を具体的にし，設計上の制約を洗い出し，さらに，SMTソルバであるYicesを用いて，それらの制約を設計が充足しているかどうかを検証する手法を提案する．