あっちに書いたんですが...(こぴぺ
http://mentai.2ch.net/test/read.cgi/infosys/1011618439/83

83：非決定性名無しさん ：02/02/13 09:28
基礎となる数学理論、というのはよく分かりませんが、
・状態遷移　　　　ペトリネットとかオートマトンとの対比
・仕様記述・検証　意味論の記述に集合論とか代数の概念を援用
とかしているのでしょうか？

＃最近のUML拡張で、OCL (Object Constraint Language)
＃による事前条件・事後条件の記述機能が追加され、
＃　http://www.amazon.co.jp/exec/obidos/ASIN/0201379406/ref=sr_aps_d_1_1/250-4956143-4769858
＃状態遷移の検証等が可能らしいですが、
＃きちんとした仕様記述・検証には 言語Z を使用するという方もおられるそうです。
＃
＃「UMLの意味論」をきちんと扱おうとすると、別の形式的仕様記述が必要そうですね。