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.
Detta Java-program kan sedan valideras med en modellkontroll som Java Pathfinder REF ].
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']}