Abstrakt. Denna uppsats beskriver en översättare som heter Java PathFinder (Jpf), som översätter från Java till Promela, modellspråket för Spin-modellkontrollen. Jpf översätter ett givet Java-program till en Promela-modell, som sedan kan kontrolleras med hjälp av Spin. Java-programmet kan innehålla påståenden, som översätts till liknande påståenden i Promela-modellen. Snurrmodellens kontroll kommer då att leta efter dödläge och överträdelser av angivna påståenden. Jpf genererar en Promela-modell med samma rymdegenskaper som Java-programmet. Därför måste Javaprogrammet ha ett ändligt och traktat tillståndsutrymme. Detta arbete bör ses i ett bredare försök att göra formella metoder tillämpliga inom NASA:s områden som rymd, luftfart och robotik. Arbetet är en fortsättning på ett försök att formellt analysera, med hjälp av Spin, ett flertrådigt operativsystem för Deep-Space 1 rymdfarkost, och av tidigare arbete med att tillämpa befintliga modellkontroller och teorem bevis för verkliga tillämpningar.
Java PathFinder REF, JPF, är en översättare från Java till Promela.
Model checking JAVA programs using JAVA PathFinder
{'venue': 'International Journal on Software Tools for Technology Transfer', 'journal': 'International Journal on Software Tools for Technology Transfer', 'mag_field_of_study': ['Computer Science']}