Vi presenterar ProB, ett valideringsverktyg för B-metoden. ProB automatiserade animeringsanläggningar gör det möjligt för användare att få förtroende för sina specifikationer. ProB innehåller även en modellkontroll och en förfiningskontroll, som båda kan användas för att upptäcka olika fel i B-specifikationerna. Vi beskriver ProB:s underliggande metodik och presenterar de viktiga aspekterna av genomförandet. Vi presenterar också empiriska utvärderingar samt flera fallstudier som belyser att ProB gör det möjligt för användare att upptäcka fel som inte är lätta att upptäcka med hjälp av befintliga verktyg.
ProB-systemet REF är en automatisk animator och modellkontroll för B-Metod.
ProB: an automated analysis toolset for the B method
{'venue': 'International Journal on Software Tools for Technology Transfer', 'journal': 'International Journal on Software Tools for Technology Transfer', 'mag_field_of_study': ['Computer Science']}