netail.net

_ [論文] シーケンス図形式の仕様記述言語 ▲

Yves Bontemps, Patrick Heymans, and Pierre-Yves Schobbens: From Live Sequence Charts to State Machines and Back: A Guided Tour.

IEEE Transactions on Software Engineering, Vol.31, No.12, pp.999-1014, December 2005.

Live Sequence Chart (LSC) というシーケンス図の変種を，オブジェクト（エージェント）間のメッセージ通信の仕様記述に使って，そこからオブジェクトごとの動作を作って，両方を使って検証しようというアプローチ（理想はオブジェクトごとの動作を自動生成だけど）．

LSC は，普通のシーケンス図に相当する existence LSC (eLSC) と，事前動作（Prechart）に対するリアクション（Main Chart）を記述した Universal LSC (uLSC) からなる．

uLSC の記述は，起きては困るイベント列が起きないこと（safe）と，起こるべきイベントがいつか必ず起こること（live）の両方を記述している．

そこで，オブジェクト（エージェント）ごとの振舞い記述を用意して，その出力メッセージ系列に対する safe と live の性質を調べると，その uLSC の仕様に従うか検査できる．uLSC で記述された仕様を満たすようなオブジェクト（エージェント）ごとの振舞いを自動生成するのは決定不能問題らしい．