Abstrakt. De klassiska läs- och skrivproblemen har studerats ingående. Detta gäller i mindre utsträckning för reentrantversionen, där det är tillåtet att häcka låsåtgärder. Sådana bon är användbara när ett bibliotek skapas med olika förfaranden som varje start och slut med ett lås. Att tillåta häckning gör det möjligt för dessa förfaranden att ringa varandra. Vi övervägde ett allmänt använt industriellt genomförande av problemet med reentrant reader-writers. Vi modellerade den med hjälp av en modellkontroll som avslöjade ett allvarligt fel: en möjlig dödläge situation. Modellen förbättrades och kontrollerades på ett tillfredsställande sätt för ett fast antal processer. För att uppnå ett korrekt resultat för ett godtyckligt antal processer konverterades modellen till ett teoremtest med vilket den bevisats.
I REF, Reentrant Readers Writers problem är först modelleras i UPAAL modell kontroll och hittade ett möjligt dödläge scenario.
Reentrant Readers-Writers – a Case Study Combining Model Checking with Theorem Proving –
{'venue': 'FMICS', 'journal': None, 'mag_field_of_study': ['Computer Science']}