ResearchsoftwareengineerscanuseAssuranceCases(ACs)toguideVerificationandValidation(VnV)efforts.AnACisastructuredargumentthatapropertylikecorrectnessholds.WeillustratehowACscanguideVnVactivitiesviaacasestudyofsoftwareforautomaticallyextractingthe3Dsegmentationoftheaortafrommedicalimagesofthechest.TheACargumentsuggeststhatthefollowingevidenceisrequired:comparisontoapseudo-oracle;traceabilitybetweenrequirements,design,codeandtests;reviewofallartifactsbyadomainexpertwithpropercredentials;documentationofinputassumptions;andawarningthatonlyqualifiedpeopleshouldusethesoftware.Thecasestudyhighlightsthatcodeisnottheonlyartifactofinterestforbuildingconfidenceandthatmakinganexplicitdistinctionbetweensoftwareanduserresponsibilitiesisuseful.
AssuranceCases(ACs)provideastructuredargumentthatsomeproperty(likecorrectness,reproducibility,safety,etc)holds.Herewelookatargumentsforcorrectness(safetyisoutofthecurrentscope)inresearchsoftware.ThestructureoftheACdecomposesatop-levelclaimintosub-claimsthatarethemselvespotentiallydecomposed.Thehigherlevelclaimsaretoobigandtooabstracttoprove,butiftheargumentisstructuredproperly,thebottomclaimscanbesupportedwithevidence.Theevidence,togetherwithalogical,convincingargumenttojustifythedecomposition,supportsthetop-levelclaim.Therefore,theevidencerequiredshowsusexactlytheamountofVnVactivitiesneededtosupporttheAC,nomoreandnoless.
Theonlyinputfromtheuserisaboundingboxfortheregionofinterest(aorta)andtwoseedpixels,oneforascendingandonefordescendingaorta.Ifnecessary,theusercancontrolhyperparametersforRootMeanSquare(RMS)error,maximumiterations,curvaturescaling,andpropagationscaling.
Ourtopgoalis“ProgramAortaGeomRecondeliverscorrectoutputswhenusedforitsintendeduse/purposeinitsintendedenvironment,andwithinitsoperatingassumptions.”Thisgoalisdecomposedintothefollowingsub-goals:GR:therequirementsarecomplete,unambiguous,correct,consistent,verifiable,modifiableandtraceable;GI:theimplementationcomplieswithitsrequirements;GBA:allrelevantoperationalassumptionshavebeendefined;and,GA:inputssatisfytheoperationalassumptions.Whileahazardanalysisistypicallyincludedinanassurancecaseformedicalapplications,wechosetoconcentratesolelyonanassurancecaseconcerningthecorrectnessofthecalculationsandtheassociatedVnVevidencerequirements.
VnVrequiresreviewoftheusermanual,instructionvideo,requirementsdocumentation,designdocumentation,VnVplan,andcode.Reviewshouldbestructured.Wefoundwalkthroughsofthedocumentation,algorithmsandcodeuseful.
Weobservedthefollowingfromourwalkthroughs:
2\mathit{DSC}=\frac{2\mathit{TP}}{2\mathit{TP}+\mathit{FP}+\mathit{FN}}italic_DSC=dividestart_ARG2italic_TPend_ARGstart_ARG2italic_TP+italic_FP+italic_FNend_ARG(1)IV-FWarningMessageAsweinitiallyplanned,thereferencestosectionsAssumptions,DataConstraints,andSystemContextareavailableintheUserManualandUserInstructionVideo,whereweshowtheuserhowtoimportDICOMpatient’sdata,andoperateontheinputs’datatogetasegmentationresult.ThisimpliesthattherequirementsoftheevidencesE_GA.1,E_GA.2andE_GA.3aremet.AuserwhohasreadtheUserManualandwatchedtheinstructionvideoshouldknowwhatinputsarevalid.Therefore,intheAortaGeomReconsoftware,weneedtoeffectivelyguidetheusertotheUserManual,whethertheuserhasusedthissoftwarebeforeorisafirsttimeuser.
TheevidencerequiredbyanACcanbesizeable,buttheACallowstheVnVeffortstobeguidedbyapurpose.Iftheeffortistoomuch,theACargumentcanbemodifiedtorequirelessevidenceandstillkeeptheoverallargumentasconvincingasneededinitscontext.
AsampleoftheevidencetheACrequiresforthecorrectnessofAortoGeomReconfollows:
Ourcasestudyhighlightedthatcodeisnottheonlyartifactofinterestforbuildingconfidence.ThisparticularACreliesondomainexpertreviews,ratherthanformalprooforsomeothertechnique.Thedomainexpertreviewsaremoreeffectivewhentheyarestructuredandplanned.
OneareawheretheACapproachshinesismakinganexplicitdistinctionbetweenuserresponsibilitiesandsoftwareresponsibilities.FortheAutoGeomReconsoftwarewehaveanexplicitwarningsothattheuserisawareoftheirresponsibilitytoknowhowtousethesoftware.
Assurancecasesnotonlyimproveourconfidenceinresearchsoftware,theycanalsoguideoureffortssothatweonlyinvestintheVnVactivitiesthatarenecessaryforaconvincingargument.Ourcasestudyhighlightedthefollowing:
WewouldliketothankAlanWassyng,Professor,ComputingandSoftwareDepartment,McMasterUniversity,forfruitfuldiscussionsontopicsrelevanttothispaper.WewouldalsoliketothankDr.ZahraMotamed,AssociateProfessor,MechanicalEngineeringDepartment,McMasterUniversity,fortheideaofsoftwareforautomatingsegmentationoftheaorta.