Подходы к верификации моделей систем и характеристик

Сформировалась теория моделирования изменений создаваемых ПС из готовых продуктов (семейство продуктов — Product Families или Product Lines). Она включает средства формального графового представления MX, по которому осуществляется управление вариабельностью членов семейства с учетом требований и автоматизированная обработка функций системы с проведением анализа возникающих нерегулярных ситуаций и установлением соответствия между вариабельными точками программы для внесения изменений.

Метод верификации характеристик выполняется путем:

• 1) построения модели объекта. Необходимо построить модель, которая была бы адекватна верифицированному объекту. Полученная модель должна иметь небольшое число состояний, которое является условием ее эффективной проверки. Построенная модель для программных объектов имеет большое количество состояний, которые не подразделяются на управляющие и вычислительные состояния;
• 2) формулировки требований в терминах выбранной темпоральной логики. Выполнение этого этапа сталкивается с проблемами, поскольку требования должны формулироваться в терминах модели и необходимо обеспечение их адекватности начальной спецификации объекта;
• 3) верификации модели с целью проверки формальных требований. В сравнении с первыми двумя этапами этот этап достаточно хорошо автоматизирован.