概要
形式仕様記述というのは，見た目はC言語などのプログラミング言語に似たもので，「集合」や「状態」などをより厳密に書くための構文が豊富なことから，システムの仕様を，実装担当者や品質保証技術者に誤解なく伝えるのに適している，といわれています。
「形式仕様記述を使いこなせるようになると，自然言語（日本語）での記述力も上がる。エンジニアのコミュニケーション・スキルを磨く手段として有効」（p.135より要旨を引用）
「自然言語を用いて正確に仕様を記述できるような技術者を育成するのは，もっと難しい」（p.135より要旨を引用）
- VDM-SL、VDM++、RAISE/RSL、Z、B、Clear、OBJ、CafeOBJ、CASL、LOTOSなどがあります（注）VDM-SLは1996年に、Zは2002年にISOにて標準化されています。
- Z。スキーマ、操作を記述できる
- VDM++。コマンド、コマンドレスポンス ファイルシステム、セキュリティの仕様を記述できる
UMLは親しみやすい表記で、設計者の考えを説明するのに適しています。ダイヤグラムを多用することで、モデルを視覚的にとらえることができる点がUMLのメリットですが、厳密な定義ができるわけではありません。
UMLもOCLを利用して制約を記述できるように拡張されており、形式手法に近づいてきました。しかし、もともと分かりやすさを追求してきたUMLと、厳密さ・正しさを追求してきた形式手法を統合するのは難しく、現時点では別々に考える方が実用的です。UMLと形式仕様記述は同じことを表現するためのものではないので、どちらが良いということではなく、補完関係にあるといえるでしょう。
例えば、システムをマクロでとらえて抽象レベルの高いモデルを検討する部分はUMLで行います。そして、詳細化と厳密な定義は形式仕様記述で行います。複雑な並行処理におけるデッドロックの検出には形式検証を利用するなど、UMLと形式手法を組み合わせるのが効果的
関連ドキュメント
分からないことは？
最終更新：2009年06月10日 09:47
