Model checking

Получив общее представление о верификации модели (Model he king), можно поговорить о терминах и определениях. Честно говоря, эти понятия пока представляют собой мало исследованную область и были тщательно отобраны в процессе общения со многими людьми. Другими словами, была сделана попытка отделить зерна от плевел. [c.265]

Свойства и утверждения — термин свойство пришел из области верификации модели (Model he king) и означает характерное функциональное поведение устройства, которое желательно (формально) проверить, например После запроса мы ожидаем ответа в течение 10 тактов . [c.265]

Ограничения — термин пришел из области верификации модели (Model he king). В процессе формальной верификации модели устройства рассматриваются все возможные допустимые входные комбинации. Следовательно, часто возникает необходимость ограничивать входные воздействия по каким-либо признакам, в противном случае средства проверки будут сигнализировать об ошибочных отказах и нарушениях свойств устройства, которые обычно не возникают в реальных устройствах. Как и свойства, ограничения также могут быть простыми и сложными. В некоторых случаях ограничения могут быть интерпретированы как свойства, которые подлежат доказательству Например, входное ограничение первого модуля может быть также свойством выходного сигнала второго модуля, при этом выход второго модуля подключен к входу первого. Поэтому свойства и ограничения могут иметь двойственную природу Термин ограничение также используется в системах ограниченного стохастического моделирования, и в этом случае ограничение обычно применяется для обозначения диапазона значений, которые могут быть использованы для управления шиной. [c.265]

Утверждение/свойство — термин свойство пришел из области верификации модели (Model he king), и обозначает характерное функциональное поведение устройства, которое вы хотите (формально) проверить (например после запроса мы ожидаем ответа в течение 10 тактов ). Термин утверждение пришел из области моделирования, и обозначает специфическое функциональное поведение устройства, которое вы хотите наблюдать в процессе моделирования (и сигнализирует об ошибке, если такое утверждение срабатывает ). В наши дни, при использовании формальных методов и средств моделирования в унифицированных средах, термины свойство и утверждение могут взаимозаменять друг друга, то есть свойство может выступать в качестве утверждения и наоборот. [c.394]

Формальная верификация — в недалёком прошлом термин формальная верификация (проверка) для большинства инженеров являлся синонимом проверки на эквивалентность. В контексте рассматриваемого материала проверка на эквивалентность подразумевает под собой средства, которые используют формальные (строго математические) методы сравнения двух различных представлений одного устройства — скажем RTL-описания и таблицы соединений вентилей — для определения идентичности их функциональности от входов до выходов. На практике проверка на эквивалентность может рассматриваться как подкласс формальной верификации и называться верификацией модели (model he king), которая используется при анализе конечных автоматов системы для тестирования некоторых свойств устройства, которые обычно нгзывгютутверждениями. См. также Статическая формальная верификация и Динамическая формальная верификация. [c.395]

Энциклопедия по машиностроению XXL

Оборудование, материаловедение, механика и ...