Спосіб і система контролю робасності моделі фізичної системи

1. Спосіб контролю за допомогою комп'ютера робасності моделі фізичної системи, який відрізняється тим, що включає наступні етапи: - генерують дані щодо першої моделі фізичної системи за допомогою перших засобів генерування даних, причому зазначена перша модель містить набір компонентів і щонайменше один інтерфейс введення, призначений для введення значень даних, причому вказана перша модель визначена на формальній мові, що описує поведінку й функціонування кожного з указаних компонентів; - генерують, на формальній мові, дані щодо заданої властивості, якій повинна відповідати модель фізичної системи, за допомогою засобів генерування даних щодо властивості; - виконують автоматичний пошук, за допомогою засобів формальної перевірки, поєднання значень вхідних даних, при якому зазначена задана властивість не реалізується стосовно до першої моделі, для перевірки істинності зазначеної властивості; - генерують дані, на формальній мові, щодо другої моделі, за допомогою других засобів 2 (19) 1 3 93852 4 бирають з набору заздалегідь визначених несправностей. 6. Спосіб за будь-яким з пп. 1-5, який відрізняється тим, що задана властивість відображає стан або поведінку вказаної фізичної системи. 7. Спосіб за п. 6, який відрізняється тим, що задана властивість є властивістю безпеки вказаної фізичної системи. 8. Комп'ютер для контролю робасності моделі фізичної системи, який відрізняється тим, що містить: - засоби для генерування даних щодо першої моделі (10), яка визначає фізичну систему й містить набір (12) компонентів (12а, 12b, 12с) і щонайменше один інтерфейс (14) введення, призначений для введення значень вхідних даних, причому вказана перша модель визначена на формальній мові, що описує поведінку й функціонування кожного з указаних компонентів; - засоби для генерування даних щодо заданої властивості, визначеної на формальній мові, якій повинна відповідати модель фізичної системи; - засоби формальної перевірки для автоматичного пошуку поєднання значень вхідних даних, при якому задана властивість не реалізується стосовно до першої моделі, для перевірки істинності зазначеної властивості; - засоби для генерування даних щодо другої моделі (20), визначеної на формальній мові, причому друга модель відповідає першій моделі й доповнена механізмом (22) введення несправностей, коли зазначена задана властивість перевірена як істинна для першої моделі; та - засоби формальної перевірки для автоматичного пошуку поєднання несправностей, що вводяться, і/чи значень вхідних даних, при якому задана властивість не реалізується стосовно до другої моделі, причому зазначена задана властивість розглядається як істинна щодо другої моделі, коли засоби формальної перевірки не знаходять жодного поєднання несправностей, що вводяться, і/чи значень вхідних даних значень, при якому задана властивість не реалізується, причому модель фізичної системи визнають робасною до несправностей по відношенню до вказаної заданої властивості, коли зазначена задана властивість перевірена як істинна для другої моделі. 9. Комп'ютер за п. 8, який відрізняється тим, що механізм (22) введення несправностей містить інтерфейс (24) введення несправностей і засіб (26) реалізації несправностей. 10. Комп'ютер за будь-яким з пп. 8 або 9, який відрізняється тим, що фізична система являє собою електронну систему управління авіаційним двигуном, що містить два обчислювальні пристрої. Даний винахід відноситься до контролю робасності моделі фізичної системи до несправностей. Моделювання систем використовується в даний час в багатьох галузях, зокрема, в авіаційній і аерокосмічній промисловості. Наприклад, моделі фізичних систем, призначених для виконання певних функцій, розробляють для оцінки взаємодії таких систем з навколишнім середовищем. Для цього використовують апаратні або програмні засоби. Зокрема, логічні схеми виявлення несправностей, реконфігурування і резервування компонентів використовують для надання системам стійкості до несправностей. Нажаль, практично ніяка модель не в змозі врахувати всі можливі випадки. Часто випускаються з уваги ті або інші конкретні сценарії розвитку подій або припускаються помилки в логічній послідовності, внаслідок чого певна послідовність або певне поєднання несправностей може призвести до відмови всієї системи. Для вирішення подібних проблем готові системи тестують на випробувальних стендах з метою перевірки їх робасності. Проте при виявленні дефекту готової системи необхідне її повторне конструювання, пов'язане з великими витратами часу і засобів на проведення інженерноконструкторських робіт і переробку програмного забезпечення. Задача, на вирішення якої спрямований даний винахід, полягає в усуненні вказаних недоліків і в запропонуванні способу і системи контролю роба сності моделі електронної системи до несправностей. Для вирішення поставленої задачі пропонується спосіб контролю робасності моделі фізичної системи, що включає наступні етапи: - визначення першої моделі фізичної системи, що містить набір компонентів і щонайменше один інтерфейс введення, призначений для введення значень даних, причому вказана перша модель визначена на формальній мові, що описує поведінку і функціонування кожного з указаних компонентів; - визначення на формальній мові заданої властивості, якій повинна відповідати модель фізичної системи; - визначення на формальній мові другої моделі, що відповідає першій моделі і доповнена механізмом введення несправностей; і - автоматичний пошук, за допомогою засобів формальної перевірки, поєднання несправностей, що вводяться, і/чи значень вхідних даних, при якому задана властивість не реалізується. Таким чином, друга модель дозволяє розробити фізичну систему, яка є робасною до несправностей. При цьому робасність системи забезпечується до її виготовлення, що дозволяє скоротити витрати на розробку. Спосіб за винаходом дозволяє перевірити властивості системи, враховуючи різні поєднання несправностей і/чи значень вхідних даних системи. 5 Він також дозволяє, шляхом повної перевірки всіх передбачуваних несправностей і поєднань несправностей, реалізувати систему дуже високої якості, що володіє оптимальною захищеністю. Згідно з однією з особливостей винаходу механізм введення несправностей включає введення щонайменше однієї несправності в другу модель за допомогою інтерфейсу введення несправностей. Згідно з іншою особливістю винаходу механізм введення несправностей додатково включає опис на формальній мові діяння вказаної щонайменше однієї несправності на функціонування або поведінку кожного з указаних компонентів указаної електронної системи. Задана властивість вважається істинною для другої моделі, якщо засоби формальної перевірки не знаходять жодного поєднання несправностей, що вводяться, і/чи значень вхідних даних, при якому задана властивість не реалізується. В цьому випадку модель фізичної системи вважається робасною по відношенню до вказаної заданої властивості. Задана властивість вважається хибною для другої моделі, якщо засоби формальної перевірки знаходять щонайменше одне поєднання несправностей, що вводяться, і/чи значень вхідних даних, при якому задана властивість не реалізується. В цьому випадку дане поєднання несправностей, що вводяться, і/чи значень вхідних даних, відповідає сценарію, що дозволяє виправити модель фізичної системи для підвищення її робасності. В оптимальному варіанті поєднання несправностей вибирають з набору наперед визначених несправностей. Задана властивість відображає стан або поведінку вказаної фізичної системи. Вона може бути властивістю безпеки вказаної фізичної системи. Інші особливості і переваги способу і системи за винаходом стануть зрозумілі з нижченаведеного опису, що приводиться з посиланнями на додані креслення і такого, що не накладає будь-яких обмежень. На кресленнях: фіг. 1 зображає в перспективі апаратні засоби, що використовуються в системі або способі за винаходом; фіг. 2 вкрай схематично зображає першу модель розробки фізичної системи за винаходом; на фіг. 3 представлена блок-схема, що ілюструє основні етапи визначення достовірності першої моделі за фіг. 2; фіг. 4 вкрай схемно зображає другу модель, яка відповідає першій моделі фізичної системи і доповнена механізмом введення несправностей; на фіг. 5 представлена блок-схема, що ілюструє основні етапи контролю, згідно з винаходом, робасності моделі фізичної системи до несправностей; фіг. 6 вкрай схематично зображає першу модель електронної системи, що включає, згідно з винаходом, моделі першого обчислювального пристрою, другого обчислювального пристрою і з'єднання; 93852 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, залежно від змінних або сигналів моделі. Визначена таким чином властивість звичайно є властивістю безпеки типу “така подія ніколи не відбудеться”, але може також бути і властивістю, що характеризує реакцію, типу “з такого стану можна за кінцевий час перейти в такий інший стан”. Крім того, дана влас 7 тивість повинна відповідати деякій характеристиці першої моделі або описувати її. Формальна мова володіє засобами формальної перевірки, такими, наприклад, як “система формальної перевірки” або “перевірочний пристрій” в програмі 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, до якої додані додаткові булеві 93852 8 канали введення і процедури обробки, кількість яких відповідає кількості передбачуваних несправностей. Канал введення кожної несправності може приймати значення “істинно” і “хибно”. Наприклад, значення “хибно” може відповідати стану “несправність не введена”, а значення “істинно” - стану “несправність введена”. Коли всі канали введення інтерфейсу 24 введення несправностей мають значення “хибно”, друга модель 20 працює в номінальному режимі. Коли один з каналів введення несправностей приймає значення “істинно”, він включає логічний механізм реалізації несправностей відповідного компоненту згідно зі схемою поведінки даного компоненту. Крім того, якщо будь-який канал введення несправностей вільний, засоби формальної перевірки можуть у будь-який момент ввести несправність для пошуку послідовності або поєднання несправностей і/чи значень вхідних даних, які можуть викликати невідповідність деякій заданій властивості. Засоби формальної перевірки є системою, яка застосовує логічні правила до аксіом і/чи схем поведінки компонентів 12а, 12b, 12с другої моделі 20 до тих пір, поки не буде отримана формула, що описує дану властивість. Ці засоби формальної перевірки можуть бути реалізовані у вигляді програми типу SILDEXТМ, яка у будь-який момент моделювання може призвести до несправності якого-небудь компоненту або функції другої моделі 20 за допомогою механізму 22 введення несправностей. А саме, для перевірки деякої властивості другої моделі 20 запускають динамічну компіляцію на формальній мові типу SILDEXТМ. Якщо компіляція завершується успішно, дана властивість вважається перевіреною. В протилежному випадку засоби формальної перевірки видають сценарій, що містить послідовність несправностей і/чи значень вхідних даних, яка приводить модель системи в стан, що суперечить даній властивості. На фіг. 5 представлена блок-схема, що ілюструє основні етапи контролю робасності моделі фізичної системи до виникнення несправностей. На етапі Е11 другу модель 20, що відповідає першій моделі 10, доповненої механізмом введення несправностей, описують (визначають) на формальній мові. Потім визначають, чи зберігається деяка властивість, яка визначена на етапі Е2 блок-схеми фіг. 2, справедливість якої для першої моделі 10 вже була підтверджена (на етапі Е4), також і для другої моделі 20. Для цього на етапі Е13 перевіряють справедливість даної властивості по відношенню до всіляких поєднань несправностей, що вводяться, і/чи вхідних даних. На цьому етапі засоби формальної перевірки проводять автоматичний пошук поєднань несправностей, що вводяться, і/чи вхідних даних, при яких задана властивість не реалізується. Якщо засоби формальної перевірки не знаходять поєднання несправностей, що вводяться, і/чи вхідних даних, при якому задана властивість не 9 реалізується, дану властивість вважають істинною. Після цього, на етапі Е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, а стрілка F2 - сигнали або дані (позначені на мові Signal символом S_2_1), що надходять від другого обчислювального пристрою 112b до першого обчислювального пристрою 112а. На фіг. 7 зображена друга модель 120 фізичної системи, що відповідає першій моделі 110 за фіг. 6 і доповнена механізмом 122 введення несправностей, які містять інтерфейс 124 введення несправностей і засіб 126 реалізації несправностей. В даному прикладі засіб 126 реалізації несправностей є засобом переривання, що імітує одиночну несправність, у тому числі у вигляді роз 93852 10 риву сполучного дроту, короткого замикання дротів або відключення з'єднання 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 відповідно. 11 Аналогічним чином, якщо в другий сполучний пристрій 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^= 8C_e^= SD_e I) I); 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 I) I). 93852 12 В загальному випадку при моделюванні фізичної системи, що містить два обчислювальні пристрої, можна досліджувати наступні дві властивості: “модель системи не ідентифікує себе при обох обчислювальних пристроях в активному стані” і “модель системи не ідентифікує себе при обох обчислювальних пристроях в пасивному стані”. Крім того, можна передбачити моделювання ситуації наявності одиночної несправності при включенні системи. В цьому випадку можна перевірити, чи не набуває система вищеописаної властивості в результаті присутності одиночної несправності при включенні системи. Крім того, може бути передбачено моделювання виникнення одиночної несправності функціонування системи при одночасному включенні обох обчислювальних пристроїв. При цьому передбачається, що будь-яка одиночна несправність може виникнути у будь-який момент. Для цього канал введення даної несправності може бути залишений вільним, а всій решті каналів може бути присвоєно значення “хибно”. Несправності можуть бути вибрані з наперед визначеного набору несправностей, що містить наступні несправності: несправностей немає; негативний результат автоматичного тестування; обрив; коротке замикання; обрив каналу передачі; з'єднання не підключено; збій синхронізації; несправність NVM встановлена на значення “хибно”; несправність NVM встановлена на значення “істинно”; несправність сигналу PPAVM встановлена на значення “хибно”; несправність сигналу PPAVM встановлена на значення “істинно”; PPAVMTBP; відмова обчислювального пристрою; несправність сигналу РН встановлена на значення “хибно”; несправність сигналу РН встановлена на значення “істинно”; і т.д. Таким чином, винахід дозволяє контролювати робасність моделі до несправностей до виготовлення фізичної системи, що дозволяє виготовити систему, яка володіє оптимальною захищеністю, і скоротити витрати на розробку цієї системи. Зрозуміло, що винахід також дозволяє контролювати робасність вже виготовленої фізичної системи. В цьому випадку фізичну систему моделюють моделлю, що складена на формальній мові, і перевіряють робасність моделі системи до відмов, як описано вище, по критеріях, що відповідають певним властивостям системи. 13 93852 14 15 93852 16 17 Комп’ютерна верстка Мацело В. 93852 Підписне 18 Тираж 23 прим. Міністерство освіти і науки України Державний департамент інтелектуальної власності, вул. Урицького, 45, м. Київ, МСП, 03680, Україна ДП “Український інститут промислової власності”, вул. Глазунова, 1, м. Київ – 42, 01601