2024年5月3日发(作者：)

AComponent-basedApproachtoVerifiedSoftware:

What,Why,HowandWhatNext?

Kung-KiuLau,ZhengWang,AnduoWangandMingGu

SchoolofComputerScience,TheUniversityofManchester

ManchesterM139PL,UnitedKingdom

kung-kiu,zw@

SchoolofSoftware,TsinghuaUniversity,Beijing,China

wad04@,guming@

1What?

Ourcomponent-basedapproachtoverifiedsoftwareisaresultofcross-fertilisationbe-

tweenverifirasttoap-

proachesbasedoncompositionalverificationtechniques,ourapproachisdesignedto

solvethescaleprobleminverifiedsoftware.

Compositionalverificationtendstobetop-down,itionsasystemintosub-

systems,andprovesthewholesystembyprovingthesubsystems(Fig.1).Thesubsys-

System spec

SubspecSubspec

. . .

System proof

Proof ofProof of

. . .

subsyssubsys

itionalverification.

tems,oftencalledcomponents,aresystem-specific,andarethereforenotintendedfor

owsthattheirproofscannotbereusedinothersystems.

Bycontrast,ourapproachtoverifiedsoftwareisbottom-up,startingwithpre-existing

pre-verifiedcomponents,andcomposingthemintoverifiedcomposites.(Fig.2).Com-

Composite componentComposite component proof

ComponentComponent

. . .

proofproof

. . .

VerifiedVerified

componentcomponent

ent-basedapproachtoverifiedsoftware.

ponentsaresystem-independent,

proofsarethereforealsoreusableindifferentsystems.

2Why?

Incompositionalverification,theonlyformof‘scalingup’isdecompositionintosmaller,

kofdecompositionitself(andcomposingthe

subproofs)isdirectlyproportionaltothesizeofthewholesystem.

Bycontrast,inourcomponent-basedapproach,scalingupisachievedbecauseeach

alnumber

ofcompositionstepsrequireddependsonthesizeofthewholesystemaswellasthe

granularityofthecomponents.

3How?

Thepre-requisiteforacomponent-basedapproachtoverifiedsoftwareisthatcompo-

nentsandtheirspecification,compositionandverificationarenotonlywell-defined,

butalsodefinedinsuchawaythatverifiedsoftwarecanbebuiltinacomponent-based

,weneedacomponentmodelsuchthatitsupportsthisapproach.

3.1AComponentModel

Acomponentmodeldefineswhatcomponentsare,

havedefinedacomponentmodel[7]inwhichwecanalsoreasonaboutcomponentsand

finingcharacteristicsofourcomponentsareencapsulation

andcompositionality,finingcharacteristicofour

compositionoperatorsisthattheyareexogenousconnectors[8]thatprovideinterfaces

tothecompositestheyproduce.

sthat

ourcompositecomponentshavehierarchicalspecifications,hierarchicalproofobliga-

tions,orverificationconditions(VCs),andasaresult,proofreuse,viasub-VCs,is

possible.

3.2ACaseStudy:TheMissileGuidanceSystem

WehaveimplementedourcomponentmodelinSpark[2],andusingthisimplemen-

tation,wehaveexperimentedonanindustrialstrengthcasestudy,aMissileGuidance

system[4],sileGuid-

ancesy

consistsofamaincontrolunitandinput//Ohandlerreadsdatafromdiffer-

nits

thenpasstheirresultstoanavigationunitwhichproducestheoutputforthesystem.

Theimplementationin[4]contains246packagesincludingtoolsandatestharness.

Intotal,ithas30,102linesofSparkAdacodeincludingcommentsandannotations.

Usingourcomponentmodel,wehaveimplementedacomponent-basedversionof

edcodefrom

[4]ascomputationunits,1,Seq1’,

Seq2andSeq4arecompositecomponentswhoseinterfacesaresequenceconnectors.

3isa

sequenceconnector,Sel1aSelector,Pipe1andPipe2arepipeconnectorsandLoopis

aniterator.

Wehaveprovedthesystemcompletely,usingtheSparkprooftools:Examiner,Sim-

plifierandChecker;mary

2