Model Extraction for ARINC 653 based Avionics Soft

ModelExtractionforARINC653basedAvionicsSoftware?PedrodelaC´amara,Mar´ıadelMarGallardo,andPedroMerino1UniversityofM´alagaCampusdeTeatinoss/n,29071,M´alaga,[e-mail],{gallardo,pedro}@lcc.uma.esAbstract.Oneofthemostexcitingandpromisingapproachestoensurethecorrectnessofcriticalsystemsissoftwaremodelchecking,whichcon-sidersrealcode,writtenwithstandardprogramminglanguageslikeC.Onegeneraltechniquetoimplementthisapproachisproducingareducedmodelofthesoftwareinordertoemployexistingandefficienttools,likespin.Thispaperpresentstheapplicationofthetechniquetoavionicssoftwareconstructedontopofanapplicationinterface(api)compliantwiththearinc653specification(apex),whichiswidelyemployedbythemanufacturersintheavionicsindustry.Thepaperusesmodellingtech-niquespreviouslydevelopedbytheauthors.However,thesetechniquesarenowextendedtodealwithnewproblems,likereal-timeaspectsandscheduling.Thepaperalsocontainsanoveltestingmethodtoensurethecorrectnessofthekeypartinthemodel:theexecutionenginethatim-plementsapexservices.Thistestingmethodusesspintoexecuteofficialtestsuites.Keywords:Modelextraction,softwaremodelchecking,avionics,apex,RealTime1IntroductionApplicationsoftwareforavionics,rangingfromcomfortandmeasurementsoft-waretocriticalflyingcontrolsystems,arecurrentlyimplementedontopofasharednetworkofprocessorsfollowingstandardinterfaceslikearinc653(Avion-icsApplicationSoftwareStandardInterface)[1].Theapplicationsshareproces-sors,memoryanddevices(sensorsandinput/outputdevices)andthewholesystemrequiresspecificschedulingmethodswithrealtimefeatures.Sothever-ificationofthiskindofsystemisarealtrendformodelcheckerpractitioners.Itiswellknownthatonemajorproblemofmodelcheckingfornon-experten-gineersisthatthetechniquerequiresadeepunderstandingofboththemodellingandthepropertylanguagessupportedbythetools.Furthermore,themanualconstructionprocessissusceptibletohumanerrorsduetomisunderstandingsor?ThisworkhasbeenpartiallysupportedbytheSpanishMECundergrantTIN2004-7943-C04plainprogrammingbugs.Thisisonereasontostartmanyprojectsthatcangen-eratesuitablemodelswithminimalhumaninteraction(seeFeaver[9],JPF1[7]andBandera[4]).In[6]and[5],theauthorsdevelopamodelextractiontech-niquetodealwithsoftwarebuiltontopofwelldefinedapis.Theapproachwasimplementedforspin4(thesametargetasthatofotherrelatedtoolslikeFeaVerorBandera).Inthispaper,weextendandapplyourmethodtoverifyCapplicationsrunningontopofapex.Themainextensionstoourpreviousworkconsistinmodellingtimefeaturesandusingconformancetestingforcheckingthecorrectnessofourmodel.Modellingandverificationofavionicssoftwareisalsodescribedin[10].Theproblemofmodellingrealtimeinspinhasbeenconsideredin[3].Although,adetailedcomparisonwiththeseworksisgiveninSection8,wemaysummarizethemaincontributionsofthispaperasfollows:1.Themethodtomodeltimingeventspreservesthesizeofthestatespaceintothelimitssuitableforverificationwithspin,like[3].Inaddition,ourapproachcanalsobenefitfromabstractmatching.2.Theapproachin[10]isorientedtotheverificationoftheoperatingsystem(os),andnottotheapplicationsrunningontopofthisos.Wemodelboththeosandtheapplicationand,inparticular,wefocusondebuggingtheapplication.Furthermore,ourmodelofthearincexecutionengineisalsoavailablefortraditionalhand-mademodellingoftheapplications.3.Insofarastheverificationoftheapplicationdependsonthecorrectnessofthemodeloftheos,weautomaticallycheckthecorrectnessofourarincmodel.Tothisend,weemployspintodoautomatictesting,usingtheofficialtestsuitesavailableintheavionicsindustry.Thepaperisorganizedasfollows.ThepreliminarymaterialinSection2summarizesourgeneralextractionapproachtodealwithsoftwareconstructedontopofwell-definedapis[6].Section3givesanoverviewoftheapexapiandthepartitioningschemeforavionicssoftware.ThemainideasofthemodelextractionapproacharepresentedinSection4andthedetailsoftimemodellinginSection5.SomeexperimentalresultsthatconfirmthefeasibilityofthemethodisgiveninSection6.Section7showsthecorrectnessofourapproachthroughtesting.Sections8and9concludewithamoredetailedcomparisonwithrelatedworks,andtheconclusions,respectively.2ModelextractionwithWell-definedAPIsExistingapproachestoverifyingsoftwarebymodelextractiondonotspecificallyaddresstheproblemofhowtomodelservicesprovidedbytheoperatingsystem.Theyaresuitableforsourcecodethatonlycontainslibraryfunctionsthatcanbeexecutedbythetargetmodelchecker(seeFeaver[7]).Whenthetargetmodelcheckercannotdirectlyexecutealltheoperatingsystemcalls,itisnecessarytoaddsomeextrahardnesstocompletetheextractedmodels.2Clientsandservers(Ccode)globalvarsmain(){LocalvarsCblock;APIcall;............Cblock;APIcall;}Functionsglobalvarsmain(){LocalvarsCblock;APIcall;............Cblock;APIcall;}FunctionsAdditionalCglobalvars;proctypep1(){CglobalvarsClocalvars;Cblock;APIcall;............Cblock;APIcall;}proctypep2(){Cblock;APIcall;............Cblock;APIcall;}Clientsandservers(Pormelacode)Fig.1.MappingschemeinSocketMCIn[6]weconsideredhowtoverifyconcurrentCapplicationsthatmakeexten-siveuseofosfacilitiesthroughsystemcalls.Inourapproachtomodelextraction,weconstructaspinorientedmodelo