взаимодействующих друг с другом, а также в системах, обладающих структурами данных, способных принимать большое число значений.
Моделирование. Первая задача заключается в приведении проектируемой системы к такому формальному виду, который был бы приемлем для инструментальных средств верификации моделей программ. Во многих случаях это просто задача компиляции. В других случаях, при органичениях по времени и объему памяти, моделирование может потребовать абстракции, чтобы избавиться от несущественных деталей, не относящихся к делу.
Спецификация. Перед проведением верификации нужно сформулировать свойства, которыми должна обладать проектируемая системы. Обычно спецификации задаются на языке формальной логики. Для аппаратуры и программного обеспечения, как правило,