Parameterized Verification of Synchronized Concurrent Programs
Zeinab Ganjei · Linköping studies in science and technology. Dissertations · 2021
POPULÄRVETENSKAPLIG SAMMANFATTNINGSamtidiga program består av flera processer som deltar i beräkningar.Sådana processer kan, jämfört med de sekventiella varianterna, resultera i mer effektiva och tillförlitliga program.Sensornätverk som sprids i en skog för att larma om eld, inbyggda system som möjliggör användningen av olika funktioner i en modern bil eller banksystem som delar transaktioner och beräkningsbelastning på olika processorer är några exempel på system som kan köra samtidiga program.Att kontrollera att samtidiga program är korrekta, dvs.att de beter sig som förväntat, är en komplex uppgift på grund av deras invecklade beteende och det, möjligtvis, stora antalet inblandade processer.Buggar och logiska misstag i datorprogram kan orsaka mänskliga och materiella förluster.Verkliga skräckexemplen inkluderar fall där synkroniseringsfel mellan processer som kontrollerar delar av en strålbehandlingsmaskin resulterade i strålningsöverdoser för flera patienter.Att försäkra sig att samtidiga program beter sig som förväntat är därför viktigt.Formell verifiering och testning är två huvudmetoder för analys av datorprogram.Vid testning ges en uppsättning testfall som input till programmet.För varje testfall anges också det förväntade resultatet.Sedan jämförs programmets resultat mot det förväntade resultatet.Testning är väl etablerat och kan upptäcka många buggar till en låg kostnad.Testning kan dock inte bevisa att ett program är korrekt.Formell verifiering är en samling av tekniker som syftar till att bevisa programkorrekthet.Modellkontroll (model checking) är en formell verifieringsteknik som är lämplig för samtidiga program.Korrektheten är uttryckt med hjälp av formler i temporallogik.Själva verifieringen genomförs med hjälp av en uttömmande sökning av systemets beteende.Tekniken introducerades ursprungligen för att verifiera samtidiga program med ändligt antal tillstånd.Att utöka modellkontroll till system med godtyckliga tillståndstorlek är ett aktivt forskningsområde.I denna avhandling fokuserar vi på formell verifiering av parametriserade system.Det vill säga, system där antalet processer är ändligt men inte begränsas på förhand.Vi tillhandahåller helautomatiska och parametriserade modellkontrolltekniker för att etablera eller motbevisa säkerhetsegenskaper (safety properties) för valda klasser av samtidiga program.Vi presenterar våra experimentella resultat genom flera exempel.Först beaktar vi problemet med att automatiskt kontrollera säkerhetsegenskaper för phaser-program där antalet processer kan vara avgränsade eller parametriserade.Dessa samtidiga program använder sig av phasers: en komplex synkroniseringskonstruktion som implementeras i moderna språk som Habanero Java.För det avgränsade fallet fastställer vi avgörbarhet för att kontrollera om programuttryck respekteras och oavgörbarhet av att kontrollera dödläge-frihet.För det parametriserade fallet studerar vi olika formuleringar av verifieringsproblemet och föreslår en exakt procedur som garanteras avslutas för vissa nåbarhetsproblem även med obegränsade antal phaser och godtyckligt många uppkomna processer.Vi föreslår också en metod för automatisk verifiering av parametriserade program där variabler delas och manipuleras av flera processer.Vi introducerar predikat som använder speciella variabler som hänvisar till antalet processer som uppfyller vissa givna egenskaper och vanliga variabler som direkt manipuleras av det samtidiga programmet.Detta möjliggör att resonera kring relationen mellan antalet processer med vissa egenskaper och värden i programvariablerna.Dessutom introducerar vi Lazy Constrained Monotonic Abstraction för effektivare utforskning av välstrukturerade abstraktioner av icke-monotona system.Dessa är system där instanser med flera processer inte nödvändigtvis behöver kunna göra mera än instanser med färre processer.Det gör att analysen av parametriserade varianter blir svårare.Vi föreslår flera heuristik och jämför deras effektivitet med hjälp av omfattande experiment med vår öppenkällkod prototyp.Till slut föreslår vi en sund men (i allmänhet) icke-fullständig procedur för automatisk verifiering av säkerhetsegenskaper för en klass av fel-toleranta distribuerade protokoll som beskrivs i Heard-Of-modellen.Vi föreslår en verifieringsheuristik iv som garanteras avslutas även för ett obegränsat antal processer som kör det distribuerade protokollet.v I want to begin by thanking God for He has given me the opportunity and capability to reach this stage of my life.Then, I would like to offer my sincere gratitude to my advisors, Associate Professor Ahmed Rezine, Professor Petru Eles, and Professor Zebo Peng for giving me the opportunity to pursue a PhD in the Embedded Systems Lab at Linköping University, for sharing their wisdom and knowledge, and most importantly, for allowing me the room to work in my own way.I cannot thank any of my professors enough for their dedication and efforts in creating an excellent working environment.Their input, understanding, and patience have been invaluable in helping me pursue my research goals.I am especially