Способ и система контроля робастности модели физической системы

Изобретение относится к системе и способу контроля робастности модели физической системы. Техническим результатом является обеспечение способа и системы контроля робастности модели физической системы к неисправностям. Способ включает этапы: определение первой модели физической системы, содержащей набор компонентов и, по меньшей мере, один интерфейс ввода, предназначенный для ввода значений данных, причем первая модель определена на формальном языке, описывающем поведение и функционирование каждого из указанных компонентов; определение, на формальном языке, заданного свойства, которому должна соответствовать модель физической системы; определение, на формальном языке, второй модели, соответствующей первой модели и дополненной механизмом ввода неисправностей; и автоматический поиск сочетания вводимых неисправностей и/или значений входных данных, приводящего к несоответствию указанному заданному свойству, при помощи средств формальной проверки. 2 н. и 11 з.п. ф-лы, 8 ил.

 

Область техники, к которой относится изобретение

Настоящее изобретение относится к контролю робастности модели физической системы к неисправностям.

Уровень техники

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

Способ и система формирования и контроля эффективности модели физической системы (преимущественно электронной программируемой системы), которые могут быть выбраны в качестве ближайших аналогов соответственно способа и системы по настоящему изобретению, описаны в патентном документе ЕР 1117044, М. Кл. G06F 11/25, 18.07.2001.

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

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

Раскрытие изобретения

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

Для решения поставленной задачи предлагается способ контроля робастности модели физической системы, включающий следующие этапы:

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

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

- определение, на формальном языке, второй модели, соответствующей первой модели и дополненной механизмом ввода неисправностей; и

- автоматический поиск, при помощи средств формальной проверки, сочетания вводимых неисправностей и/или значений входных данных, при котором заданное свойство не реализуется.

Таким образом, вторая модель позволяет разработать физическую систему, робастную к неисправностям. При этом робастность системы обеспечивается до ее изготовления, что позволяет сократить расходы на разработку.

Способ по изобретению позволяет проверить свойства системы, учитывая различные сочетания неисправностей и/или значений входных данных системы.

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

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

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

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

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

В оптимальном варианте сочетание неисправностей выбирают из набора заранее определенных неисправностей.

Заданное свойство отражает состояние или поведение указанной физической системы. Оно может быть свойством безопасности физической системы. В частном случае физическая система может представлять собой электронную систему, например, такую как электронная система управления авиационным двигателем.

Краткое описание чертежей

Другие особенности и преимущества способа и системы по изобретению станут ясны из нижеследующего описания, приводимого со ссылками на прилагаемые чертежи и не налагающего каких-либо ограничений. На чертежах:

- фиг.1 изображает в перспективе аппаратные средства, используемые в системе или способе по изобретению;

- фиг.2 крайне схематично изображает первую модель разработки физической системы по изобретению;

- на фиг.3 представлена блок-схема, иллюстрирующая основные этапы определения достоверности первой модели по фиг.2;

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

- на фиг.5 представлена блок-схема, иллюстрирующая основные этапы контроля, в соответствии с изобретением, робастности модели физической системы к неисправностям;

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

- фиг.7 крайне схематично изображает вторую модель, соответствующую первой модели по фиг.6 и дополненную механизмом ввода неисправностей;

- фиг.8 крайне схематично изображает механизм ввода неисправностей по фиг.7.

Осуществление изобретения

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

Компьютер 1 содержит обычные для устройств такого типа аппаратные средства. Более конкретно компьютер содержит центральный блок 2, выполняющий последовательности команд программного обеспечения, соответствующего способу по изобретению, центральное запоминающее устройство 3, сохраняющее данные исполняемых программ, носители цифровых данных (жесткий диск, дисковод для компакт-дисков 4 и т.д.), обеспечивающие длительное хранение данных и программного обеспечения, периферийные устройства ввода (клавиатуру 5, мышь 6 и т.д.), а также периферийные устройства вывода (экран 7, печатающее устройство и т.д.), обеспечивающие отображение модели физической системы.

На фиг.2 изображена первая модель 10 физической системы, соответствующая изобретению. Физическая система может быть, например, электронной системой, предназначенной для поддержки определенного приложения, например, контроля и управления органами регулировки двигателя.

Первая модель 10 содержит набор 12 компонентов 12а, 12b, 12с, взаимодействующих друг с другом, по меньшей мере, один интерфейс 14 ввода, предназначенный для ввода входных данных, и, по меньшей мере, один интерфейс 16 вывода. Разумеется, набор 12 компонентов может быть задан на определенном уровне абстракции, зависящем от уровня точности или подробности моделирования физической системы.

Первая модель 10 представляет собой численную модель, отображающую архитектуру разрабатываемой физической системы. Ее описывают на формальном языке типа «Signal», содержащем алфавит переменных, логические кванторы и логические коннекторы и, таким образом, описывающем поведение и функции каждого из компонентов 12а, 12b, 12с. Благодаря этому первая модель 10 позволяет реализовать динамическое представление физической системы.

На фиг.3 представлена блок-схема основных этапов определения достоверности первой модели 10.

На этапе Е1 на формальном языке описывают (определяют) первую модель.

Затем, на этапе Е2, на формальном языке описывают также некоторое заданное свойство, которым должна обладать модель физической системы. Формальная запись такого свойства сводится к определению события, соответствующего этому свойству, и к кодированию этого события, например, на языке Signal, в зависимости от переменных или сигналов модели. Определенное таким образом свойство обычно является свойством безопасности типа «такое-то событие никогда не произойдет», но может также быть и свойством, характеризующим реакцию, типа «из такого-то состояния можно за конечное время перейти в такое-то другое состояние». Кроме того, данное свойство должно соответствовать некоторой характеристике первой модели или описывать ее.

Формальный язык обладает средствами формальной проверки, такими, например, как «система формальной проверки» или «проверочное устройство» в программе SILDEX™, предназначенными для семантической проверки истинности свойства, определенного по отношению к любым входным данным или их сочетаниям, вводимым в первую модель.

Так, этап Е3 заключается в проверке истинности заданного свойства по отношению к всевозможным сочетаниям входных данных. На этом этапе средства формальной проверки производят автоматический поиск такого сочетания входных данных, при котором это заданное свойство не реализуется.

Если средства формальной проверки не находят такого сочетания входных данных, при котором заданное свойство не реализуется, то на следующем этапе Е4 первая модель 10 рассматривается как достоверная по отношению к этому свойству.

Если же данное заданное свойство признано ложным, т.е. если на этапе Е3 средства формальной проверки находят, по меньшей мере, одно сочетание входных данных, при котором заданное свойство не реализуется, происходит переход на этап Е5.

На этапе Е5 создают диагностику, содержащую последовательность входных данных, при котором заданное свойство не реализуется.

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

На фиг.4 крайне схематично изображена вторая численная модель 20 по изобретению, соответствующая первой модели 10, но дополненная механизмом 22 ввода неисправностей.

Вторая модель 20 отличается от первой модели 10 тем, что она, помимо набора 12 компонентов 12а, 12b, 12с, интерфейса 14 ввода и интерфейса 16 вывода, содержит механизм 22 ввода неисправностей, включающий в себя интерфейс 24 ввода неисправностей, через который вводят, по меньшей мере, одну неисправность или сочетание неисправностей, и средство 26 реализации неисправностей.

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

Другими словами, механизм 22 ввода неисправностей содержит составленное на формальном языке описание воздействия или воздействий любых неисправностей на функционирование или поведение каждого из компонентов 12а, 12b, 12с второй модели 20 физической системы.

Таким образом, вторая модель 20 соответствует первой модели 10, к которой добавлены дополнительные булевы каналы ввода и процедуры обработки, количество которых соответствует количеству предполагаемых неисправностей. Канал ввода каждой неисправности может принимать значения «истинно» и «ложно». Например, значение «ложно» может соответствовать состоянию «неисправность не введена», а значение «истинно» - состоянию «неисправность введена».

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

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

Средства формальной проверки представляют собой систему, которая применяет логические правила к аксиомам и/или схемам поведения компонентов 12а, 12b, 12с второй модели 20 до тех пор, пока не будет получена формула, описывающая данное свойство.

Эти средства формальной проверки могут быть реализованы в виде программы типа SILDEX™, которая в любой момент моделирования может вызвать неисправность какого-либо компонента или функции второй модели 20 при помощи механизма 22 ввода неисправностей.

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

На фиг.5 представлена блок-схема, иллюстрирующая основные этапы контроля робастности модели физической системы к возникновению неисправностей.

На этапе Е11 вторую модель 20, соответствующую первой модели 10, дополненной механизмом ввода неисправностей, описывают (определяют) на формальном языке.

Затем определяют, сохраняется ли некоторое свойство, определенное на этапе Е2 блок-схемы фиг.2, справедливость которого для первой модели 10 уже была подтверждена (на этапе Е4), также и для второй модели 20.

Для этого на этапе Е13 проверяют справедливость данного свойства по отношению к всевозможным сочетаниям вводимых неисправностей и/или входных данных. На этом этапе средства формальной проверки производят автоматический поиск сочетаний вводимых неисправностей и/или входных данных, при которых заданное свойство не реализуется.

Если средства формальной проверки не находят сочетания вводимых неисправностей и/или входных данных, при котором заданное свойство не реализуется, данное свойство считают истинным. После этого, на этапе Е14, модель физической системы признают робастной к неисправностям в отношении данного свойства.

Если же средства формальной проверки находят на этапе Е13, по меньшей мере, одно сочетание вводимых неисправностей и/или входных данных, вызывающее противоречие данному свойству, то данное свойство признают ложным, после чего, на этапе Е15, средства формальной проверки создают диагностику. Эта диагностика содержит сценарий или последовательность значений входных данных в интерфейсах ввода 14, 24 неисправностей и входных значений, которые приводят к нежелательной ситуации.

На этапе Е16 производят анализ диагностики, т.е. изучают последовательность операций со второй моделью 20 и моменты ввода неисправностей. Этот анализ позволяет пересмотреть конструкцию модели физической системы или же показать, что воспроизведение сценария, выявленного средствами формальной проверки, маловероятно.

Фиг.6-8 иллюстрируют упрощенный пример контроля робастности модели физической системы.

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

На фиг.6 изображен пример первой модели 110 физической системы, моделирующей первое вычислительное устройство 112а (которое содержит первый интерфейс 114а ввода и первый интерфейс 116а вывода), второе вычислительное устройство 112b (которое содержит первый интерфейс 114b ввода и первый интерфейс 116b вывода) и соединение 112с между вычислительными устройствами (которое содержит соединительные провода, обеспечивающие двустороннюю связь, или обмен данными, между первым вычислительным устройством 112а и вторым вычислительным устройством 112b). Стрелка F1 обозначает сигналы или данные (обозначенные на языке Signal символом S_1_2), передаваемые первым вычислительным устройством 112а второму вычислительному устройству 112b, a стрелка F2 - сигналы или данные (обозначенные на языке Signal символом S_2_1), поступающие от второго вычислительного устройства 112b к первому вычислительному устройству 112а.

На фиг.7 изображена вторая модель 120 физической системы, соответствующая первой модели 110 по фиг.6 и дополненная механизмом 122 ввода неисправностей, который содержит интерфейс 124 ввода неисправностей и средство 126 реализации неисправностей. В данном примере средство 126 реализации неисправностей представляет собой средство прерывания, имитирующее одиночную неисправность, в том числе в виде разрыва соединительного провода, короткого замыкания проводов или отключения соединения 112с. Стрелка F1a обозначает сигналы S_1_2, поступающие от первого вычислительного устройства 112а, а стрелка F1b - сигналы S_2_1_v, попадающие во второе вычислительное устройство 112b после прохождения через средство 126 реализации неисправностей. Стрелка F2b обозначает сигналы S_2_1, поступающие от второго вычислительного устройства 112b, а стрелка F2a - сигналы S_1_2_v, попадающие в первое вычислительное устройство 112а после прохождения через средство 126 реализации неисправностей. В отсутствие неисправности сигнал, поступающий от первого вычислительного устройства 112а или от второго вычислительного устройства 112b, попадает соответственно во второе вычислительное устройство 112b или в первое вычислительное устройство 112а. При наличии же неисправности сигнал, поступающий от одного из вычислительных устройств 112а, 112b, не достигает своего назначения. В языке Signal это выражается следующими уравнениями:

S_1_2_v=S_1_2 when not неисправность.

S_2_1_v=S_2_1 when not неисправность.

На фиг.8 крайне схематично изображен механизм ввода неисправностей и, в частности, средство 126 реализации неисправностей по фиг.7. Это средство 126 реализации неисправностей содержит первый канал 124а ввода неисправности, соответствующий ситуации «соединение не подключено», и второй канал 124b ввода неисправности, соответствующий ситуации «обрыв соединительного провода». Первый и второй каналы 124а, 124b ввода неисправностей присоединены к входам логической схемы 132 «или». Выход этой логической схемы соединен с первым средством 134 соединения/разрыва, разрешающим или запрещающим передачу сигналов от первого вычислительного устройства 112а ко второму вычислительному устройству 112b, и со вторым средством 136 соединения/разрыва, разрешающим или запрещающим передачу сигналов от второго вычислительного устройства 112b к первому вычислительному устройству 112а.

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

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

Так, если в первое соединительное устройство 134 не введена неисправность, входные сигналы SA_e, SB_e, SC_e и SD_e равны соответственно выходным сигналам SA_s, SB_s, SC_s и SD_s этого соединительного устройства 134. При этом первое соединительное устройство 134 разрешает пересылку сигналов SA_1_2, SB_1_2, SC_1_2 и SD_1_2, передаваемых от первого вычислительного устройства 112а ко второму вычислительному устройству в форме сигналов SA_1_2_v, SB_1_2_v, SC_1_2_v и SD_1_2_v соответственно.

Аналогичным образом, если во второе соединительное устройство 136 не введена неисправность, входные сигналы SE_e, SF_e, SG_e и SH_e равны соответственно выходным сигналам SA_s, SB_s, SC_s и SD_s этого соединительного устройства. При этом второе соединительное устройство 136 разрешает пересылку сигналов SE_1_2, SF_1_2, SG_1_2 и SH_1_2, передаваемых от второго вычислительного устройства 112b к первому вычислительному устройству 112а в форме сигналов SE_1_2_v, SF_1_2_v, SG_1_2_v и SH_1_2_v соответственно.

Если первый канал 124а ввода неисправности, соответствующий ситуации «соединение не подключено», и/или второй канал 124b ввода неисправности, соответствующий ситуации «обрыв соединительного провода», свободны, средства формальной проверки или проверяющее устройство в любой момент может ввести отключение соединения и/или обрыв соединительного провода. В этом случае сигнал или сигналы, передаваемые одним из вычислительных устройств 112а, 112b, не достигают второго вычислительного устройства.

По окончании этапа инициализации приведенный выше пример может быть записан на языке Signal в следующей форме:

process xxx_process_sildex_1=

(? boolean SA_e, неисправность, SB_e, SC_e, SD_e;

| boolean SA_s, SB_s, SC_s, SD_s;)

(| (| SA_s=SA_e when not неисправность

| SB_s=SB_e when not неисправность

| SC_s=SC_e when not неисправность

| SD_s=SD_e when not неисправность

| неисправность ^=SA_e^=SB_e^=SC_e^=SD_e

|)

|);

process xxx_process_sildex_2=

(? boolean SE_e, неисправность, SF_e, SG_e, SH_e;

| boolean SE_s, SF_s, SG_s, SH_s;)

(| (| SE_s=SE_e when not неисправность

| SF_s=SF_e when not неисправность

| SG_s=SG_e when not неисправность

| SH_s=SH_e when not неисправность

| неисправность ^=SE_e^=SF_e^=SG_e^=SH_e

|)

|).

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

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

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

Неисправности могут быть выбраны из заранее определенного набора неисправностей, содержащего следующие неисправности: неисправностей нет; негативный результат автоматического тестирования; обрыв; короткое замыкание; обрыв канала передачи; соединение не подключено; сбой синхронизации; неисправность NVM установлена на значение «ложно»; неисправность NVM установлена на значение «истинно»; неисправность сигнала PPAVM установлена на значение «ложно»; неисправность сигнала PPAVM установлена на значение «истинно»; PPAVMTBP; отказ вычислительного устройства; неисправность сигнала РН установлена на значение «ложно»; неисправность сигнала РН установлена на значение «истинно»; и т.д.

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

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

1. Способ контроля робастности модели физической системы, отличающийся тем, что включает следующие этапы:
определение первой модели (10) физической системы, содержащей набор (12) компонентов (12а, 12b, 12с) и, по меньшей мере, один интерфейс (14) ввода, предназначенный для ввода входных значений данных, причем указанная первая модель определена на формальном языке, описывающем поведение и функционирование каждого из указанных компонентов;
определение на формальном языке заданного свойства, которому должна соответствовать модель физической системы;
автоматический поиск при помощи средств формальной проверки, сочетания значений входных данных, при котором заданное свойство не реализуется;
определение на формальном языке второй модели (20) физической системы, соответствующей первой модели и дополненной механизмом (22) ввода неисправностей в случае, если заданное свойство проверено как истинное по отношению к первой модели; и
автоматический поиск при помощи средств формальной проверки, сочетания вводимых неисправностей и/или значений входных данных, при котором заданное свойство не реализуется по отношению ко второй модели (20), причем указанные средства формальной проверки выполнены с возможностью применения логических правил к аксиомам и/или схемам поведения набора (12) компонентов (12а, 12b, 12с); и
определение, что указанная модель физической системы является робастной, по отношению к неисправностям, относящимся к заданному свойству, если средства формальной проверки не обнаруживают никакого сочетания введенных неисправностей и/или значений входных данных, для которых заданное свойство не реализуется по отношению ко второй модели (20).

2. Способ по п.1, отличающийся тем, что механизм (22) ввода неисправностей включает ввод, по меньшей мере, одной неисправности во вторую модель (20) при помощи интерфейса (24) ввода неисправностей.

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

4. Способ по п.1, отличающийся тем, что заданное свойство считается истинным для второй модели (20), если средства формальной проверки не находят ни одного сочетания вводимых неисправностей и/или значений входных данных, при котором заданное свойство не реализуется.

5. Способ по п.4, отличающийся тем, что если заданное свойство считается истинным для второй модели, модель физической системы считается робастной по отношению к указанному заданному свойству.

6. Способ по п.1, отличающийся тем, что заданное свойство считается ложным для второй модели (20), если средства формальной проверки находят, по меньшей мере, одно сочетание вводимых неисправностей и/или значений входных данных, при котором заданное свойство не реализуется.

7. Способ по п.6, отличающийся тем, что указанное сочетание вводимых неисправностей и/или значений входных данных соответствует сценарию, позволяющему исправить модель физической системы для повышения ее робастности.

8. Способ по п.1, отличающийся тем, что сочетание неисправностей выбирают из набора заранее определенных неисправностей.

9. Способ по любому из пп.1-8, отличающийся тем, что заданное свойство отражает состояние или поведение указанной физической системы.

10. Способ по п.9, отличающийся тем, что заданное свойство является свойством безопасности указанной физической системы.

11. Система контроля робастности модели физической системы, отличающаяся тем, что содержит:
первую модель (10), определяющую физическую систему и содержащую набор (12) компонентов (12а, 12b, 12с) и, по меньшей мере, один интерфейс (14) ввода, предназначенный для ввода значений входных данных, причем указанная первая модель определена на формальном языке, описывающем поведение и функционирование каждого из указанных компонентов;
заданное свойство, определенное на формальном языке, которому должна соответствовать модель физической системы;
средства формальной проверки для автоматического поиска сочетания значений входных данных, при котором предварительно заданное свойство не реализуется;
вторую модель (20) физической системы, определенную на формальном языке, причем вторая модель соответствует первой модели и дополнена механизмом (22) ввода неисправностей, и указанная вторая модель (20) определяется в случае, если заданное свойство проверено как истинное по отношению к первой модели;
и средства формальной проверки для автоматического поиска сочетания вводимых неисправностей и/или значений входных данных, при котором указанное предварительное заданное свойство не реализуется по отношению ко второй модели, причем указанные средства формальной проверки выполнены с возможностью применения логических правил к аксиомам и/или схемам поведения набора (12) компонентов (12а, 12b, 12с), и при этом указанная модель физической системы определяется как робастная по отношению к неисправностям, относящимся к заданному свойству, если средства формальной проверки не обнаруживают никакого сочетания введенных неисправностей и/или значений входных данных, для которых заданное свойство не реализуется по отношению ко второй модели (20).

12. Система по п.11, отличающаяся тем, что механизм (22) ввода неисправностей содержит интерфейс (24) ввода неисправностей и средство (26) реализации неисправностей.

13. Система по п.11 или 12, отличающаяся тем, что физическая система представляет собой электронную систему управления авиационным двигателем, содержащую два вычислительных устройства.