Abstrakt. De senaste rapporterna om olyckor riktar uppmärksamheten på "automatiseringsöverraskningar" som uppstår i säkerhetskritiska system. En automationsförvåning kan uppstå när ett system beter sig annorlunda än operatörens förväntningar. Förändringar i gränssnittsläget är en klass av sådana överraskningar som har stor betydelse för säkerheten hos ett dynamiskt interaktivt system. De kan ske implicit till följd av andra systemåtgärder. Formella specifikationer för interaktiva system ger möjlighet att analysera problem som uppstår i sådana system. I det här dokumentet tar vi hänsyn till den roll som en interaktionsbaserad specifikation har som en partiell modell av ett interaktivt system så att lägets konsekvenser kan kontrolleras tidigt i designprocessen. Vi visar hur interaktionsspecifikationer kan översättas till SMV-modellens indataspråk och hur vi kan använda sådana specifikationer tillsammans med modellkontrollen för att analysera risken för förväxling i ett realistiskt fall. Vårt slutliga mål är att utveckla en allmän metodik för automatiserad analys av interaktiva system. Denna kontrollprocess kan vara till nytta när det gäller att ta upp frågor som måste behandlas i ett bredare analyssammanhang.
I REF användes modellkontroll för att modellera och bevisa egenskaper hos specifikationer för interaktiva system så att eventuella oväntade konsekvenser av gränssnittsändringar kan kontrolleras tidigt i designprocessen.
Model Checking Interactor Specifications
{'venue': 'Automated Software Engineering', 'journal': 'Automated Software Engineering', 'mag_field_of_study': ['Computer Science']}