«Математика-2» и формирование решений задач

Прежде всего, до 1998 г. считалось, что корректные и некорректные по качеству математического решения задачи образуют два базовых класса, четко отделенных друг от друга. Однако, на протяжении ряда лет исследуя методы формального синтеза систем управления и причины неустойчивости синтезируемых систем, Петров обнаружил третий, пограничный класс задач, способных изменять корректность в ходе преобразования при их решении. Результаты были опубликованы в работе «Неожиданное в математике...» и других, в частности, в книге /8/.

В частности, существуют такие системы уравнений, решения которых не обладают свойством непрерывной зависимости от параметров. Корректность может изменяться, даже если все преобразование состоит в перестановке местами уравнений в системе относительно исходного их порядка.

Исходя из сказанного, вводится понятие об эквивалентности математических преобразований в расширенном смысле – т.е. как неизменения корректности решаемой задачи в ходе этих преобразований. Для конкретных классов задач далеко не все преобразования, эквивалентные в традиционном (узком) смысле, эквивалентны и в расширенном; в связи с этим возможно, что формально правильное решение задачи будет фактически неверным.

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

Свойства использованных преобразований следует рассматривать в комплексе: математическая модель – задача (в физическом смысле) – выбранный метод её решения. Решение некорректных задач следует проверять контрольными примерами при вариациях исходных данных. На практике это не всегда возможно; поэтому для определенных задач применяют специальные методы проверки решений и приемы преобразований, сохраняющие эквивалентность в расширенном смысле.

В дальнейших своих работах Петров разработал общие приёмы установления корректности и частные их приложения к математической формализации задач различных классов. Всё это он назвал собирательным термином «Математика-2».

Отметим, что эти идеи были предвосхищены видным отечественным учёным-палеонтологом, мыслителем и литератором И.А. Ефремовым. В своём романе «Туманность Андромеды» (1957) он ввёл т.н. биполярную математику, которая должна отражать диалектический подход в количественно-формальном знании. В качестве составляющей этой математики Ефремов ввёл и определил т.н. репагулярное исчисление как формальное исследование переходов количественных характеристик предмета изучения в его новое качество. Из определения видно, что Математика-2 фактически может рассматриваться как разновидность такого исчисления применительно к переходам количества погрешностей решения задачи в качество корректности метода решения.

С точки зрения ключевых идей нашего курса, подобный результат можно рассматривать как подтверждение одного из главных положений «китайской» диалектики: «сущность является в форме». Недопустимое изменение формы приводит к тому, что математическая запись перестает отражать сущность описываемых явлений. Кроме того, мы сталкиваемся с системной триадой «модель-задача-метод», где каждый компонент существен для результата.

Проверка моделей и формальная верификация

Формальная верификация активно развивается с 1970-х годов, но ряд ключевых результатов, существенных для её практического применения, получен на рубеже веков. По материалам работы /Карпов Ю.Г., БХВ-Петербург, 2010, Гл.1/, в настоящее время известны три направления:

Подробнее остановимся на третьем направлении.

Сущность метода – проверка того, что на данной формальной модели выполняется (принимает истинное значение) заданная логическая формула. При этом система моделируется системой переходов с конечным числом состояний. Используя т.н. темпоральные логики – неклассического («псевдофизического») рода с участием времени – выражают требуемые свойства поведения системы точно и недвусмысленно. Тогда верификация сводится к исчерпывающему анализу пространства состояний модели, не требующему логического вывода, и потому м.б. автоматизирована.

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

Практический смысл имеют спецификации, количественно отражающие временные свойства систем (т.к. реальная система как минимум взаимодействует со внешней средой и обычно в ней совместно протекают ряд процессов), а часто – также и вероятностные (когда моделируются системы стохастические). Это потребовало некоторых новых математических средств.

Искусственные системы (в т.ч. информатические), для которых внешняя среда выступает не просто как производитель исходных объектов (данных) и потребитель результатных, а как взаимодействующая сущность (которая в п/п 4.1.5.1 названа реальной средой исполнения), определены Карповым как реагирующие¹ (а по Паронджанову – «реального времени»). Такая среда (окружение) должна представляться как совместно протекающий процесс (система взаимодействующих процессов), взаимодействующая с процессом (системой процессов), протекающим[и] в рассматриваемой системе; механизмы взаимодействия в техноязыке обсуждались нами в п/п 4.1.6.2.

Изначально построенные темпоральные логики были «чёткими», т.е. подразумевали выполнение свойств с вероятностью 0 или 1; время же в них имело «философско-грамматический» смысл периодизации на «прошлое/настоящее/будущее», задаваемой различными отношениями порядка между «точкой свершения» некоего события, «точкой говорения» о нём и «точкой референции», т.е. моментом, на который ссылается высказывание. Это в общем соответствует временам в естественных языках². Были выделены два класса таких логик: линейного времени (LTL) и ветвящегося времени (CTL). В первом классе будущее для каждого времени (состояния верифицируемого процесса перед очередным переходом) единственное; тем самым отражается одно возможное вычисление (маршрут алгопроцесса). Во втором классе допускается альтернативный выбор (развилка) в любом состоянии; тем самым отражается потенциальная множественность будущего протекания алгопроцесса. В любом случае это логики качественного анализа.

В дальнейшем были построены количественные логики вероятностного типа (Probabilistic) с возможностью «размытых» суждений о выполнении свойств, а также временного типа (Timed) с привязкой к реальному времени (числовым шкалам, примерно так, как по таймеру в ДРАКОНе-2). Они относятся к классу CTL.

Важно понимать, что названные классы логик несводимы друг к другу; т.о. для выражения разных свойств нужно использовать логики из соответствующих классов.

Возможно проверять свойства следующих видов:

Каждый вид свойств м.б. формально определён в той или иной темпоральной логике (но необязательно в каждой); кроме того, Карпов в Гл. 6 своей работы приводит формулировки конкретных свойств каждого вида.

Каково содержание процесса верификации по методу Model checking? Можно определеить его как следующую процедуру:

Спецификация м.б. задана как описание структуры переходов, что требует высокой квалификации специалиста. В то же время сегодня стало возможным описывать процессы на императивных языках спецификаций высокого уровня (напоминающих языки параллельного программирования); инфорсима поддержки верификации автоматически строит по такой спецификации структуру переходов. Можно формировать спецификацию, так сказать, «снизу вверх» – анализируя и абстрагируя уже созданную систему, и «сверху вниз» – как укрупнённое описание будущей системы.

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

Элементарная верификация по данному методу математически заключается в поиске на развёртке структуры переходов маршрутов, на которых не выполняется то или иное заданное свойство. Для разных логик используются разные методы такого поиска; автоматизация обеспечивается алгоритмическим представлением метода на конечных структурах данных (т.е. фактически информатизацией модели).

Анализ результата связан с определением по контрпримеру причин его существования. В связи с неадекватностью модели и реальной системы возможно, что контрпример не относится к последней, т.е. является артефактом абстрагирования системы. Если контрпример относится и к системе, то необходимо определить и устранить причины его появления; тем самым возвращаемся к фазе создания/совершенствования.

Разработан ряд ModelChecking-систем, автоматизирующих верификацию³. Они используют собственные входные языки представления, обычно уникальные для каждой системы; сегодня все они текстовые.

Отметим, что существует ограничение на сложность модели для автоматизированного анализа; однако уже можно проверять довольно сложные реальные системы.

Как же в целом можно оценить формальную верификацию вообще и метод проверки моделей в частности на современном этапе развития? Достоинства состоят в том, что:

Всё это означает, что качество верификации напрямую зависит от квалификации персонала. Специалист по формальной верификации должен:

Ясно, что это требует глубокого понимания реальной системы и процессов её абстрагирования.

Метод проверки моделей позволяет сосредоточить внимание верификатора на специфицировании системы и анализе результатов. Поэтому по сравнению с неавтоматизируемыми методами он, безусловно, является шагом вперёд. Его недостатки скорее имеют место по отношению к некоей идеальной ситуации, когда любой специалист в сфере проверяемой деятельности мог бы без особых затрат на повышение квалификации начать работать по этому методу. Тем не менее такую ситуацию следует считать желательной по той же причине, что и автоформализацию профессиональных знаний – коль скоро доказательность должна стать обычным явлением, то «отдельных» верификаторов рано или поздно станет нехватать. Для рядового же «предметника» часто деятельность даже по данному методу окажется чересчур сложной.

Что можно сказать о допустимости того уровня абстрагирования, который необходим для нынешних ModelChecking-систем? Атомизация детальных визуалов принципиально не ограничивает разработку; можно вводить её как свёртку дракон-руководства (инструкции, программы) до дракон-спецификации (фактически имеет место подгонка спецификации, изначально формулируемой по критериям формализации эскиза, под критерии атомарности переходов в реагирующих системах). Механизмы реального времени и взаимодействия в техноязыке аналогичны языкам ModelChecking-систем (с точностью до формы представления). Более существенны ограничения типологии величин для верификации. В частности, это касается допустимости только целых числовых типов; единственно очевидный путь – переход в модели предметной области от вещественных чисел к целым с выбором достаточной разрядности.

А как формальная верификация связана с тестированием? Оно как процесс установления качества разработки имеет свои достоинства и недостатки, как и верификация. Следует считать эти два процесса взаимодополняющими.

2 Поэтому, кстати, наименование изначально определённой темпоральной логики по-английски – TL – расшифровывается как Tense, а не Time Logic, как можно было бы предположить.