О верификации простых автоматных программ на основе метода Model Checking

Аннотация

В статье применительно к простым автоматным программам (их поведение описывается одним конечным автоматом) излагается техника верификации, которая базируется на темпоральных логиках и называется Model Checking. Для автоматных программ удается автоматизировать процесс построения модели программы, подлежащей верификации.