摘要
Inthispaper,aschemeofcombiningmodelcheckingandtheoremprovingtechniquestoverifyhightrustworthyembeddedsoftwareisproposed.Thesoftwaremodeldescribedinstatemachineofunifiedmodellanguageistransformedintotheinputmodelinglanguageofamodelcheckerinwhichthemodelisanalyzedwithassociatedpropertyspecificationsexpressedintemporallogic.Thesoftwaremodelwhichhasbeenverifiedbymodelcheckeristhentransformedintoabstractspecificationsofatheoremprover,inwhichthemodelwillberefined,verifiedandtranslatedintosourceCcode.Thetransformationrulesfromstatemachinetoinputlanguageofmodelcheckerandabstractspecificationsoftheoremproveraregiven.Theexperimentshowsthattheproposedschemecaneffectivelyimprovethedevelopmentandverificationofhightrustworthyembeddedsoftware.
出版日期
2005年04月14日(中国期刊网平台首次上网日期,不代表论文的发表时间)