Verification of a microcomputer program specification embedded in a reactive system
Yasunori Ishihara, Kiichiro Ninomiya, Hiroyuki Seki, Daisuke Takahara, Yutaka YAMADA, Shigesada Omoto · 2000
this paper) iscon2;Dq:FT whichrepresen ts the behavior of a given program,an then given properties (or re uiremen ts) of the program are verifiedon the reachability graph.On of the advan tages of model checkin is that the verification procedurecan be fully automatic, whileon of the disadvan tages is that the size of a reachability graphoften becomesin tractably large (the so-called state explosion problem). However, sinq computers are rapidly becomin more powerful these days, model checkin has succeededin the fields of hardwaredesign communmqC8DC protocols, etc. Basedon [10], we have developed a formal specification