资源描述：
《Formal methods _ Practice and experience.pdf》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。
1、FormalMethods:PracticeandExperienceJIMWOODCOCKUniversityofYork19PETERGORMLARSENEngineeringCollegeofAarhusJUANBICARREGUISTFCRutherfordAppletonLaboratoryandJOHNFITZGERALDNewcastleUniversityFormalmethodsusemathematicalmodelsforanalysisandverificationatanypartoftheprogramlife-c
2、ycle.Wedescribethestateoftheartintheindustrialuseofformalmethods,concentratingontheirincreasinguseattheearlierstagesofspecificationanddesign.Wedothisbyreportingonanewsurveyofindustrialuse,comparingthesituationin2009withthemostsignificantsurveyscarriedoutoverthelast20years.We
3、describesomeofthehighlightsofoursurveybypresentingaseriesofindustrialprojects,andwedrawsomeobservationsfromthesesurveysandrecordsofexperience.Basedonthis,wediscusstheissuessurroundingtheindustrialadoptionofformalmethods.Finally,welooktothefutureanddescribethedevelopmentofa
4、VerifiedSoftwareRepository,partoftheworldwideVerifiedSoftwareInitiative.Weintroducetheinitialprojectsbeingusedtopopulatetherepository,anddescribethechallengestheyaddress.CategoriesandSubjectDescriptors:D.2.4[SoftwareEngineering]:Software/ProgramVerification—Asser-tioncheckers
5、,classinvariants,correctnessproofs,formalmethods,modelchecking,programmingbycontract;F.3.1[LogicsandMeaningsofPrograms]:SpecifyingandVerifyingandReasoningaboutPrograms—Assertions,invariants,logicsofprograms,mechanicalverification,pre-andpost-conditions,specificationtech-niqu
6、es;F.4.1[MathematicalLogicandFormalLanguages]:MathematicalLogic—Mechanicaltheoremproving;I.2.2[ArtificialIntelligence]:AutomaticProgramming—ProgramverificationGeneralTerms:Documentation,Experimentation,Management,Measurement,Reliability,Theory,Verifi-cationAuthors’addresses:J
7、.Woodcock,DepartmentofComputerScience,UniversityofYork,Heslington,YorkYO105DD,UK;P.G.Larsen,EngineeringCollegeofAarhus,DouglasAvenue2,8000AarhusC,Denmark;J.Bicarregui,STFCRutherfordAppletonLaboratory,HarwellScienceandInnovationCampus,Didcot,OxfordshireOX110QX,UK;J.Fitzgera
8、ld,SchoolofComputingScience,NewcastleUniversity,New-castleuponTyne,NEI7RU,UK;Corresponden
