i. our coursenew

《i. our coursenew》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、1LogicinComputerScience:tool-basedmodelingandreasoningaboutsystemsMichaelHuthDepartmentofComputingandInformationSciencesKansasStateUniversityManhattan,KS66506-2302Abstract-Recentyearshavebroughtaboutthedevelopmentofunderstandhowtoevaluateitsformulasovertheircorrespond-powerfultoolsforver

2、ifyingspecificationsofhardwareandsoft-ingnotionofmodels.Wealsodiscussitsprooftheoryandprovewaresystems.Bynow,majorcompanies,suchasIntel,IBM,importantquantifierequivalences.(3-4weeks).AT&T,Siemens,andBThaverealizedtheimpactandimpor-3.Verificationbymodelchecking.Protocols,networks,andtanceofs

3、uchtoolsintheirowndesignandimplementationpro-distributedsystemscangenerallynotbedescribedbycodeofcessesasameansofcopingwiththeever-increasingcomplexitysomedeterministicprogramminglanguage.Suchsystemsex-ofchipandsoftwaredesigns.Thisnecessitatestheavailabilityhibitconcurrentbehaviorandthey

4、aretypicallyreactiveintheofabasicformaltrainingthatallowsUndergraduatestudentstosensethattheirbehaviordependsonwhattheenvironmentcangainsufficientproficiencyinusingandreasoningwithsuchtool-offer(e.g.“Istheprinterbusy?”).Computationtreelogic(CTL)animatedframeworks.Wepresentanexistingcourse,

5、“LogicaliscurrentlyoneofthepopularframeworksusedinverifyingFoundationsofProgramming”,thataimsatmeetingtheseedu-propertiesofconcurrentsystems.Westudyitssyntaxandse-cationalgoals.Afterdescribinginherentchallengesthatsuchamantics,andusethoseinsightstodesignanautomatedverifica-coursefaces,wet

6、henevaluatethiscourseinthelargercontexttionalgorithmwhichtakesadescriptionofasystemandspeci-ofwhatlogicalframeworks,ifany,shouldbetaughtandwhereficationsofexpectedbehaviorasinputandcheckswhetherthattheymaybeplacedinacomputer-sciencerelatedundergradu-systemmeetsthoseexpectations.Thatalgori

7、thmisthefounda-atecurriculum.tionforatool,thesymbolicmodelverifier(SMV)[20],whichweusetoevaluatesomebasicdesigns,e.g.simpleelevatorsys-I.OURCOURSEtemsandamutualexclusionprotocol(3-4weeks).4.ProgramVerification.Givenaprogram,writteninA.Missionstatementandcoursedescriptionso