順序回路の代数的仕様とその検証-モジュール数がパラメータ化されている場合-(共著)

侯 豫榕
佐藤 洋一郎
杉山 裕二
岡本 卓爾

同一モジュールを複数個含む順序回路では,モジュール数がパラメータ化されることがあり,また満たすべき性質もモジュール数がパラメータ化されたまま与えられることがある.本論文では,そのような順序回路と性質を対象に,モジュール数がパラメータ化されたままの状態で行うことのできる代数的検証法について検討し,検証が可能であるための十分条件を示している.この十分条件は,同一モジュール群の接続関係が同型であることなどを含んでいる.また,この十分条件の最用例として,リングアービタの抽象的動作の仕様を代数的に記述し,それが満たすべき二つの性質である"相互排他性"と"ノーデッドロック性"の検証を行っている.

電子情報通信学会論文誌(DI)

一般社団法人電子情報通信学会

J76-D-I

11

594

603

http://ci.nii.ac.jp/naid/110003315850
http://ci.nii.ac.jp/ncid/AN10071319
http://id.ndl.go.jp/bib/3845835