> -- Драконограф писал(а):
> Вообще это та же проблема обеспечения "тематического обзора" модели (т.е. возможности дать при сочинении закрытый перечень её состояний при исполнении), что решалась и в model checking. В принципе очевидный путь выбран при реализации этого метода в средах автоверификации - ввести конечные множества типов, сочетания которых при исполнении (имитации исполнения) можно перебрать и проверить на соответствие логическим требованиям. Также можно поступить и для представления самой модели программы (кстати, её текстовая форма просто менее удобна для наглядного описания, чем "графитная" - сама по себе возможность описания от формы, конечно, не зависит - только от конечности модели).А может быть все дело в том, что... задача ставится некорректно?.. Есть интерфейсы, и любая сущность, обладающая требуемым набором интерфейсов, может выступать в требуемой роли (собственно, роль, в данном контексте, это поименованный набор интерфейсов). Разрабатывая/проектируя свою часть, мы оперируем не сущностями, но только ролями, абстрагируясь от сущностей (которые могут быть очень большими и многообразными), выступающих в данной роли в конкретной реализации, в конкретный момент времени. Какая разница, для компьютера, что подключено к USB-порту... для него и фотоаппарат, и флэшка, и принтер - просто USB-устройство. И если соединяемые части соблюдают требования интерфейса, то они могут вполне успешно взаимодействовать. И при создании нового USB-устройства не надо думать о тестировании всех компьютеров, в которые оно потенциально может быть воткнуто. И при создании компьютера не надо думать о тестировании всех возможных USB-устройств...
Проблемы начинаются тогда, когда реализуется не система, способная решать множество задач конкретной предметной области, а программа. Программа вырезает некоторое подмножество задач, соответственно и некоторое подмножество сущностей и связей. Тем не менее, "отрезанные" сущности и связи реально существуют и их влияние как-то надо учитывать. Сделать это, порой, совсем не просто... поскольку поведение "сохраненных" сущностей и связей становится нетривиальным, неподдающимся проверке (верификации).