6月のSEAフォーマル・メソッド分科会(SIG-FM)の月例会は、森 彰さん(JAIST)の講 演と討論を企画しました。
講演内容
本講演では，オブジェクトの動的振舞いを代数的に定義するための振舞仕様
(Behavioral Specification) の手法について解説し，システムの正当性検証がどの ように自動化されるかを例を用いて紹介する．オブジェクト指向の基本概念の形式化
についての説明を行なった後，代数仕様言語 CafeOBJ 上で開発された定理証明器 PigNose を用いたモデル検査による自動検証について触れる予定である．
参考文献
(1) Coherence for Cartesian Closed Categories: A Sequential Approach, Proc. of Forth International Workshop on Conditional and Typed Rewriting Systems CTRS'95, LNCS 968, pp.276-295, 1995.
(2) 圏によるソフトウェア意味の可視化. コンピュータソフトウェア, Vol.12, No.4, pp.72-83, 1995.
(3) Distributed Cooperative Formal Methods Tools, Proc. of IEEE Conf. on Automated Software Engineering ASE'97, pp.55-62, 1997.
(4)Verifying Behavioural Specifications in CafeOBJ Environment, Proc. of World Congress on Formal Methods FM'99, to appear, 1999.
***************** 開催要領 *****************
1. 日 時： 2000年6月 2日 (金) 13:30 〜 16:45
2. 場 所： 労働スクエア東京 502 A(和室)会議室 (東京・中央区 新富1-13-14)
3. プログラム：
13:00〜13:30 受付
13:30〜14:30
「オブジェクト指向のための形式手法 --
振舞仕様とモデル検査による自動検証について」
14:30〜15:00 質疑応答
15:00〜15:15 Coffee Break
15:15〜16:30 討論
16:30〜16:45 次回予定
17:30〜 懇親会@さがみや（予定）