Background. Open source dependencies have become ubiquitous in software development and the risk of regressions during an update are a key concern facing developers. Change impact analysis (CIA) can be used to assess the effects of a dependency update and aid in addressing this challenge. The manual effort required for CIA has created a need to reduce the amount of data that is considered during a compatibility assessment. Formal (mathematical) methods for equivalence analysis have been prolific in previous attempts at minimizing the amount of data that needs to be analyzed. C bounded model checker (CBMC) is an established tool that can perform equivalence verification and a gap in knowledge exists regarding its usefulness for assessing update compatibility. Objectives. The objective of the study was to evaluate how well CBMC could filter out equivalent changes from impact assessments and the relevance of this for dependency updates. A tool named Equivalent update filter (EUF) was developed in the study to tackle this problem. Effectiveness of the tool was assessed based on, (1) the size of reductions that were made possible through filtering, (2) the relevance of the auto-generated verification resources created to perform analysis and (3) the correctness of the results during equivalence analysis. Methods. To assess the reduction capabilities of EUF a controlled experiment regarding the effect of CBMC based equivalence analysis upon impact assessment sizes was conducted. Updates for the experiment were derived from random commit pairs among three C dependencies with established industry use. The relevance of EUF's auto-generated verification resources were measured through an ordinal scale that highlighted the prevalence of different properties in a dependency that would prevent sound equivalence analysis. Soundness of the reductions suggested by EUF was investigated through a comparison with a manually labeled set of updates. Results. The developed filtering approach was able decrease impact assessment sizes by 1 % on average. Considerable differences were observed between the dependencies in the study in regards to analysis time. For each update, 11 % of the auto-generated verification resources were found to be useful for equivalence analysis on average.EUF's classification of equivalent changes was measured to have an accuracy of 67 % in relation to the base truth of manually labeled updates. Conclusions. The study showed that EUF and by extension, CBMC based equivalence analysis, has potential to be useful in dependency compatibility assessments. Follow up studies on different verification engines and with improved methodologies would be necessary to motivate practical use. / Bakgrund. Att använda externa bibliotek med öppen källkod är praxis inom mjukvaruutveckling och risken för uppdateringar att introducera problem är ett betydande orosmoment för utvecklare. Konsekvensanalys, "Change impact analysis" (CIA), kan användas för att utvärdera effekten av en uppdatering och bemöta denna utmaning. Den manuella interaktion som krävs för CIA har medfört att mängden data som analyseras behöver begränsas. Formella (matematiska) metoder för ekvivalensanalys har varit centrala i tidigare försök att minimera analysbehov. "C bounded model checker" (CBMC) är ett etablerat verktyg för C som kan utföra ekvivalensanalys och tidigare forskning har inte studerat dess relevans för kompatibilitetsbedömning vid beroende uppdateringar. Syfte. Denna studies syfte var att utvärdera CBMC's förmåga att filtrera bort ekvivalenta ändringar från uppdateringar av externa beroenden. Verktyget "Equivalent update filter" (EUF) utvecklades under projektet för att uppnå syftet. Effektiviteten av EUF bedömdes med hjälp av tre kriterier, (1) storleken på de reduktioner som möjliggjordes av filtrering, (2) relevansen av de autogenererade resurser som skapades för att utföra ekvivalensanalys och (3) korrektheten av de resultat som erhölls från ekvivalensanalys. Metod. EUF's reduktionsförmåga undersöktes genom ett kontrollerat experiment där inverkan av CBMC baserad ekvivalensanalys på analysbehovet för olika uppdateringar analyserades. Uppdateringarna som användes för experimentet hämtades från tre olika C bibliotek med bred användning i industrin. Värdet av EUF's autogenererade resurser studerades i relation till hur ofta de medförde negativa konsekvenser på korrektheten av ekvivalensanalysen. Korrektheten hos de reduktioner som EUF utförde under experimenten mättes genom en jämförelse med ett antal manuellt klassificerade uppdateringar. Resultat. Den utvecklade filtreringsmetoden hade en förmåga att minska mängden data som behöver analyseras med 1 % i genomsnitt. Exekveringstiden varierade kraftigt mellan de olika bibliotek som testades. För varje uppdatering så bedömdes i genomsnitt 11 % av de autogenererade verifieringsresurserna vara användbara för ekvivalensanalys. EUF's detektion av ekvivalenta och icke-ekvivalenta förändringar visades ha en träffsäkerhet på 67 % i relation till manuella klassificeringar. Slutsatser. Studien fann att EUF och i förlängningen, CBMC baserad ekvivalensanalys, har potential att vara en användbar del av kompatibilitetsbedömningar för beroende uppdateringar. En uppföljningsstudie med andra verifikationsverktyg och förbättrade metoder hade varit nödvändiga för att motivera praktisk användning.
| Identifer | oai:union.ndltd.org:UPSALLA1/oai:DiVA.org:bth-23696 |
| Date | January 2022 |
| Creators | Mårtensson, Jonas |
| Publisher | Blekinge Tekniska Högskola, Institutionen för datavetenskap |
| Source Sets | DiVA Archive at Upsalla University |
| Language | English |
| Detected Language | English |
| Type | Student thesis, info:eu-repo/semantics/bachelorThesis, text |
| Format | application/pdf |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0025 seconds