Спосіб валідації системи контролю/керування

1. Спосіб валідації системи контролю/керування у реальному часі (3) промисловим процесом, де система (3) включає входи (11), зміна станів яких відображає зовнішні події (en), виходи (17), для керування зовнішніми приводами (4, 5), та автоматичні модулі (15) для виконання завдань (n) у відповідь на зовнішні події (en), та впливу на зовнішні приводи (4, 5) за допомогою виходів (11), при цьому набір станів входів та виходів у заданий момент є глобальним поточним станом (Fi) системи (3), набір станів входів та виходів, отриманих після виконання завдання (n), є стабільним глобальним станом (ESj) системи (3), при цьому спосіб валідації включає наступні стадії: - складання переліку небезпечних подій (FXj), - прогнозування в автоматичних модулях суттєвих функцій даних, згідно з принципом доповненості, - складання переліку експлуатаційних характеристик зазначених приводів (4, 5), - визначення вихідного стабільного глобального стану (ESj) системи, - на підставі вихідного стабільного глобального стану (ESj) системи моделюють разову зовнішню подію (en) для отримання результуючого стабільного глобального стану (ESj + 1), та здійснюють моделювання події (en + 1) після події (en) для отримання змодельованого стабільного глобаль 2 (19) 1 3 Даний винахід виходить з проблеми, пов'язаної із комп'ютерними системами для автоматичного контролю/керування маневровими станціями залізничних мереж та, більш детально, способів валідації таких систем. Маневрові станції залізничних мереж дозволяють мережі перемикатися для позиціонування відповідно до потреб різного ескорту потягів, що рухаються по ній, щоб постійно гарантувати безперервність руху. Переключення, які у минулому приводились в дію вручну, тепер дистанційно автоматично скеровуються системами контролю/керування, розташованими у маневрових станціях. Маневрові станції можуть самі бути зв'язані одна з одною та із централізованою станцією керування, де розташовані всі дані, необхідні для залізничного трафіку: стан мережі, теоретичні розклади (руху), позиції конвоїв та потягів, і т.д. Будь-яка механічна неоднорідність мережі, наприклад, погана позиція або наполовину відкрите переключення, буде катастрофічною та представляє неприпустимий небезпечний випадок. Це також стосується випадку роз'єднання маршрутів, що імовірно призводить до зіткнення потягу, настигання один одного або бокового ураження. Проблема експлуатаційної безпеки й безпеки комп'ютерних систем на маневрових станціях є, у такий спосіб, критичною проблемою. Сьогодні, щоб перевірити експлуатаційну безпеку маневрової станції щойно побудованої та випробуваної, або раніше працюючої станції, але на яких вже здійснюється функціональний розвиток, комп'ютерна система, яка забезпечується, спочатку піддається фазам проведення випробувань елемента, діє у відповідності до функції та від'єднана від мережі, потім, для більш глобальних тестів із послідовністю різних функцій, протягом моделювання , через моделюючу програму 30, наприклад, як показано на Фіг. 1, різноманітні сенсори та автомати 4-6 з відповідної частини мережі й стимулюючи з цього до діяльності комп'ютерну систему 3 вхідними пристроями 35, 10 й відновлюючи цим вихідні дані та дані, корисні для того, щоб здійснювати перевірку за допомогою комп'ютерного з'єднання 38. Мета таких випробувань полягає в тому, щоб гарантувати, що досягнуті автоматичні дії працюють як очікується, тобто відповідно до моделей, таких як були винайдені із використанням дизайнерських інструментів, таких як GRAFCET. Тому, це перевіряється станами вихідних даних, досягнутих автоматичними діями після проведення випробувань, виконаних із використанням дизайнерських інструментів. Тоді, перевірочні фази системи виконуються реально, цього разу система зв'язується із сенсорами та механізмами автоматичної дії, шунтами, ознаками трафіку, ... мережі, діє у відповідності до функції, тоді глобально на цілу відповідну частину мережі, тоді, можливо, у поєднанні із централізованим робочим місцем запуску. 96601 4 Проведення випробувань та перевірочних фаз визначаються командами валідації системи. Такі команди забезпечують виконання програм моделювання для моделювання та випробування програм, які мають бути виконані ними, розглядаючи так багато послідовних сценаріїв або іноді сценаріїв одночасних подій, наскільки це можливо. Тепер, згадані тут комп'ютерні системи контролю/керування розроблені для миттєвої обробки будь-якої зміни стану, виходячи з великої кількості сценаріїв випадків, що будуть розглянуті, які неможливо перелічити. Крім того, оскільки реальні тести та випробування проводяться в різних умовах застосування у дії, особливо, умовах часу, ніхто не може бути впевнений, що зміна таких умов не буде торкати достовірності валідації. Тому неможливо бути впевненим що небезпечний випадок не може трапитися. Така валідація розглянутих систем, складена із тестів та випробувань, у такий спосіб не задовольняє по двох основних причинах: і) комбінація сценаріїв є настільки велика, що повинен здійснюватись вибір та іі) фази валідації засновані на реалізаціях дій є відмінними одна від іншої. За таких умов, які б не здійснювались зусилля, ніяке повне й формальне свідчення експлуатаційної й/або цілісної безпеки комп'ютерної системи контролю/керування не може бути встановлене. І це є завдяки тому, що також намагаються досягнути, у максимально можливому ступені, такого недоступного свідчення, що, у цей час, валідація систем такого типу є неминуче довгою і дорогою. Ця проблема валідації, однак, не обмежена, у світі залізничних доріг, до єдиних систем маневрових станцій. Це може, стосуватися іншого устаткування, типу, наприклад, керування дверима вагонів. Але, більш широко, проблема відноситься до систем контролю/керування в реальному часі (переклад англійського слова "керування") у промислових процесах, незалежно від того, яка шкала часу є залученою. Таким чином, інші системи контролю/керування в реальному часі включають керівні системи будь-яких засобів руху, площин, судів..., операційних систем для атомних електростанцій або інших установок, експлуатаційних систем, і т.д. Відповідно до валідації маневрових станцій, там не можна було б допустити будь-який критичний ризик та навіть менше, будь-який катастрофічний ризик, узятий для валідації вищезазначеної системи в реальному часі. По тим же самим причинам, свідчення, що ніякий небезпечний випадок не відбувся би, не можливо було б забезпечити протягом валідації. Заявник у такий спосіб винайшов спосіб для того, щоб одержати таке свідчення протягом валідації системи в реальному часі - керівної системи для маневрової станції залізничної мережі або іншого - а також як здійснити впровадження цього винаходу. 5 Таким чином, існуючий винахід перш за все має відношення до способу валідації системи контролю/керування в реальному часі для промислового процесу, система в реальному часі включає пристрої вводу (даних), зміни стану яких є відображенням зовнішніх подій, пристрої виводу (даних), призначені для того, щоб керувати зовнішніми механізмами приводів, та автоматичними модулями, розташованими для виконання завдань у відповідності до зазначених подій та щоб діяти на зазначені механізми приводів через зазначені виводи (даних), набір станів вводів та виводів, у даний момент є поточним глобальним станом системи, набір станів вводів та виводів, одержаних, коли завдання закінчене, є стабільним глобальним станом системи, спосіб валідації, що включає наступні стадії: - встановлення списку небезпечних подій, - виведення, через взаємозалежність, істотних функцій зазначених автоматичних модулів, - встановлення списку робочих характеристик зазначених механізмів приводів, - визначення початкового стійкого глобального стану системи, - моделювання єдиного зовнішнього випадку від початкового стійкого глобального стану для одержання результуючого стабілізованого глобального стану, і - здійснення моделювання, випадок після випадку, щоб одержати стійкий глобальний стан після стійкого глобального стану, вже модельованого стійкого глобального стану. Переважніше, якщо вищезгадане описане моделювання здійснюється, поки всі можливі комбінації подій та стабільних, глобальних станів не модельовані. Якщо поточний глобальний стан отриманий для небезпечного випадку, моделювання зупиняється, і систему реального часу розглядають як неприпустиму. Якщо ніякий стійкий глобальний стан не може бути отримано виходячи із моделювання конкретного випадку та стійкого глобального стану, генерується попередження. Всі можливі зовнішні події модельовані систематично, на всіх стійких глобальних станах, які можливі, оскільки усі вони є в кінцевому числі та навіть можуть бути визначені автоматично. Дійсно, оскільки виконання завдання, що відповідає будь-якому випадку, дозволяється тільки тоді, коли ніяке завдання не виконується, всі непрогнозовані комбінації подій, які могли відбутися, у той час як завдання виконуються, усуваються. В такий спосіб немає будь-якої перерахованої комбінації подій. Завдання, що відповідають всім можливим зовнішнім подіям перевірені на всі можливі початкові стійкі глобальні стани, і вони можуть бути запущені тільки від зазначених стійких глобальних станів. Накладенням таких умов, які можуть бути суперечними до самої ідеї щодо того, яка є система в реальному часі, змінна "часу" зроблена зовнішньою до системи, як й до інших пристроїв вхідних (даних), та виключається раптове втручання цього у той час як завдання виконується. 96601 6 Тоді може бути отримана вичерпна валідація системи й у такий спосіб свідчення безпеки системи. Після моделювання, у фазі випробування, супроводжувана її обслуговуванням, система працює на тому ж самому матеріалі й/або умовах часу як зазначено вище протягом фаз проведення тестів. В такий спосіб немає ніякої різниці у проведенні фаз тестів та випробувань валідації. Щоб далі зменшувати складність системи або числа її глобальних станів, на додаток до факту, що набір вхідних глобальних станів кожного завдання є обмеженим стійкими глобальними станами, запропоновано обмежити: - моделювання підгруп часткових стійких глобальних станів, автоматично виведених з теоретичних стійких глобальних станів, - функції автоматичних модулів до таких, що дозволені відповідно до застосовних норм у промисловому процесі. Відповідно, цей винахід також відноситься до системи контролю/керування в реальному часі для промислового процесу, що включає керівний модуль, двопозиційні пристрої вводу (даних), що представляють зовнішні події та двопозиційні пристрої виводу (даних) для керування зовнішніми приводами, автоматичні модулі для того, щоб виконувати визначені заздалегідь завдання, оскільки, у відповідь на зазначені події, діють зазначені пристрої виводу (даних), набір вхідних і вихідних станів у даний момент є миттєвим глобальним станом системи, набір вхідних і вихідних станів, отриманих, коли завдання виконується, є стійким глобальним станом системи, система характеризується тим, що модуль керування розміщений так, щоб дозволити бути виконаним завданню, що відповідає будь-якому зовнішньому випадку, тільки якщо ніяке завдання, що відповідає іншому випадку, не виконується й автоматичні модулі розміщені так, щоб їхні відповідні дії приводили тільки до кінцевого числа глобальних станів. Оскільки виконання завдання, що відповідає будь-якому зовнішньому випадку дозволяється тільки якщо будь-яке завдання, що відповідає іншому попередньому випадку не виконується, всі непередбачені комбінації подій, які могли б відбутися у той час як завдання виконуються, виключаються. Краще, якщо, кожний з автоматичних модулів розміщений так, щоб його дії могли привести тільки до кінцевого числа стійких глобальних станів. Інші особливості та переваги даного винаходу стануть більш очевидним при розкритті опису надалі в цьому документі, відповідно до креслень, які додаються, на яких: - Фіг. 1 показує схему структури маневрової станції, що включає систему контролю/керування відповідно до цього винаходу та звичайну систему валідації, здатну частково реалізовувати спосіб валідації відповідно до цього винаходу; - Фіг. 2 показує основну структурну схему системи контролю/керування, якою обладнана маневрова станція; - Фіг. 3 показує схему з функціональними блоками системи контролю/керування Фіг. 2, та струк 7 туру, що повинна супроводжуватися, щоб бути валідованою відповідно до способу валідації за цим винаходом; - Фіг. 4 показує спрощену експлуатаційну схему послідовності операцій системи контролю/керування, реалізуючи структуру на Фіг. 3; - Фіг. 5 показує схему з функціональними блоками першої звичайної системи валідації, здатної реалізовувати спосіб валідації відповідно до цього винаходу; - Фіг. 6 показує схему з функціональними блоками другої кращої системи валідації, реалізуючої спосіб валідації відповідно до цього винаходу; та - Фіг. 7 показує спрощену схему послідовності операцій способу валідації відповідно до цього винаходу. Відповідно до Фіг. 1 маневрова станція 1, у поєднанні із центральною станцією РС2, від якої вона одержує експлуатаційні дані мережі, включає систему контролю/керування 3, насамперед промисловий комп'ютер, що дозволяє автоматичний контроль та керування шунтуваннями 4, автоматичне керування дорожніми знаками 5 та контроль стану мережі й руху потягів через сенсори 6. На практиці, система контролю/керування 3 включає принаймні два промислових комп'ютери. Шунтування 4 і дорожні знаки 5, надалі названі приводами 4, 5, фактично є органами, що приводять в дію такі шунтування та знаки, так само як сенсори 6, поставляючи у відповідні стани вкл/вимк, або TOR, та можливі вимірювання М є всі розташовані у межах ділянки залізничної мережі, відведеної до станції 1, РС2 є відповідальною за координацію з іншими станціями мережі, але вони також можуть бути зв'язані між собою для того, щоб спілкуватися незалежно від РС2. Комп'ютер 3 дозволяє реалізацію системи контролю/керування в реальному часі звичайного промислового процесу; тобто здатний збирати дані, типу станів TOR та вимірювань М від ділянки мережі, щоб обробити та емітувати у відповідні розпорядження TOR та можливо встановлені пункти М, забезпечується для приводів зазначеної ділянки, все це відбувається в режимі реального часу. Людино-машинний інтерфейс 9 дозволяє відображати керування, виконане при синоптичному (не показано) та людському втручанні на пульті керування (не показано), коли це, як знаходять, є необхідним. Відображення керування та втручання на пульті керування також можливо в РС2 (Фіг. 2). Щоб передати дані на комп'ютер 3 та пізніше одержувати від нього розпорядження, сенсори 6 та приводи 4, 5 електрично пов'язані з роздільником 8 електричними з'єднаннями 7 та роздільник 8 у свою чергу пов'язаний з комп'ютером 3 однієї або більше цифровими шинами 10 та можливо аналоговими з'єднаннями. Комп'ютер стимулятор 30 та комутуючий прилад 60 будуть обговорені пізніше. Відповідно до Фіг. 2, комп'ютер 3 структурований у шість рівнів: - фізичний рівень 11 для того, щоб збирати дані, що включають лінії вхідного пристрою TOR та можливі вимірювання М, що на такому рівні перетворюються в цифрові дані. Такі лінії в рівні 96601 8 11 запам'ятовують всі стани TOR, виходячи з усіх подій, що відбуваються на ділянці, що контролюються та такі події будуть згадані, надалі, як зовнішні події; - логічний рівень, зайнятий драйверами можливої периферії та насамперед блок 12 системи переривання. Блок 12 попереджає в режимі реального часу верхній рівень нижче про втручання зовнішніх подій, тобто змін стану TOR; - рівень 13 для того, щоб управляти в режимі реального часу ресурсами, типово включає модуль 13 монітору реального часу, програмне забезпечення, записане й запам'ятоване основною мовою. Монітор реального часу тримає комп’ютер 3 у режимі очікування, керуючи останнім на циклі очікування, коли немає нічого, щоб зробити та активуючи відповідні функції, коли відбувається випадок, як буде замічено пізніше; - рівень 14 для того, щоб обробляти й виконувати прикладні програми, власне кажучи інтерпретер 14 для інтерпретації, тобто перекладу у реальному часі основної мови та виконання прикладного програмного забезпечення, тобто програмного забезпечення, що записане та запам'ятоване мовою близько до функціонування маневрової станції; - рівень діаграм станів (назва, виправдання якої буде пояснена пізніше), запам'ятовуючи вищезгадане прикладне програмне забезпечення, структуроване в автоматичних модулях 15, або роботах 15. У комп'ютері 3, протягом втручання зовнішніх подій, монітор 13 робить зовнішні події доступними та активує рівень 14 інтерпретації та активації. Останній запитує та інтерпретує доречні роботи 15 по одному. Тоді такі роботи 15 емітують, на вибір, команди на приводи 4, 5 через вихідні лінії 17, і вони роблять персонал станції 1 обізнаними про випадок, мотивуючи їхній запит за допомогою синоптичного з IHM 9. Вони також запускають активацію інших роботів 15, викликаючи внутрішні події, які будуть представлені та роз'яснені далі; - рівень пам'яті 16 запам'ятовуючий глобальний стан Fi залізничної ділянки, що контролюється, та системи контролю/керування 3 з станції 1, такий стан, що обумовлює функціонування роботів 15. Використання мови прикладних програм дозволяє експлуатаційному персоналу станції 1 розуміти, або навіть змінювати, програмування роботів 15 з прикладних програм, не маючи необхідності знати основну мову, що є набагато більш неясним. Рівень інтерпретації 14 подальший включає, відповідно до Фіг. 3, блок обчислення 18, маркіруючи модулі 19 та 20 або модулі для того, щоб розміщувати події у стеках очікування 21 й 22 для того, щоб обробити події, та рівень 13 включає внутрішній годинник 23 щоб синхронізувати функціонування роботів 15 періодично в моменти Ті і поставляти інші послуги часу, більш докладно, реальні піки часу tr для моніторингу вхідних ліній 11, та модуль 24 для того, щоб представляти інформацію у синоптичному вигляді. Керівний модуль 13 включає таблицю узгодження 25 для узгодження принаймні одного ав 9 томатичного модулю 15 з будь-яким внутрішнім або зовнішнім випадком. Така таблиця дозволяє,у результаті події, знаходити робота(ів) 15 для активації у рівні діаграм станів, що містять їх. Як використовується тут, глобальний стан Fi залізничної ділянки та системи контролю та керування взагалі означає миттєвий глобальний стан Fi, що, у даному миттєвому Ті, містить набір Еі подвійних станів вхідних пристроїв TOR та керуючих пристроїв виводу (даних), за вибором зібраних вимірювань або стану їхнього порівняння щодо визначених заздалегідь порогів, всі ці стани, що відбивають послідовність зовнішніх подій (знайдено у n, що має свої значення у межах від 1 до N, розглядаючи N сенсорів TOR), що відбувається до даного моменту Ті. Зовнішній випадок en може, наприклад, бути прогоном потяга на відрізку шляху або виходу з такого відрізку, прибуття на границю шунтування, здійснюючи гарне виконання його функціонування або будь-якої іншої події, що відбувається в існуванні стану TOR. Завдання n, котре повинне бути виконане на залізничній мережі, є наслідком цього. Fi також містить набір Іі зі станів TOR, що вказує на внутрішні події (відповідно як ір, р є у межах від 1 до Р, розглядаючи такі події в числі Р) результуюче з функціонування автоматичних модулів 15. Таким чином, прикладом внутрішнього випадку ір могла бути зміна стану внутрішньої змінної, керованої одним або більше модулями робота 15, або запитом активації від робота 15, виконуваним іншим роботом 15. Миттєвий глобальний стан Fi дозволяє вивести й запам'ятати в пам'яті 27 миттєвий функціональний глобальний стан Gi щоб представляти стан системи 3 на IHM 9. Такий глобальний стан Gi є вибором або підсумком суттєвих станів зі змісту Fi, полегшуючи керівництво системою 3 експлуатаційним персоналом станції 1. Пам'ять 27 також містить стек індикаторів, отриманих з послідовних глобальних станів Gi, щоб використовуватись як журнал для службових записів або щоб допомогти керівним режимам на IHM 9. У такий спосіб миттєвий глобальний стан Fi у момент Ті представлено подвійним вектором з координатами N + Р, зовнішній миттєвий глобальний стан Еі є вектором першого N подвійного значення та внутрішній миттєвий глобальний стан Іі вектор Р зберігає подвійні значення. За допомогою пристосування проектування, такого як автоматично забезпечуються, залежно від специфікацій, схеми станів реального часу системи та набір доступних глобальних станів EGA системи відповідно до таких схем, попередньо визначене кінцеве число J специфічних глобальних станів ESj, як стабільні та надійні стани залізничної мережі. Очевидно, якщо система 3 повинна відповідати потребам станції 1, стійкі глобальні стани ESj є частиною можливих миттєвих глобальних станів Fi. Вони відповідають заключним станам завдань, замовлених системі 3 IHM 9 (або системою 3 безпосередньо) та виконаний роботами 15. 96601 10 Досягнення безпеки мережі відбувається в такий спосіб: - список робочих характеристик механізмів приводів 4, 5 установлений, підсумовуючи можливості контролю належного функціонування (наприклад, контроль шунту на правій стороні не міг привести до глобального стану, що випливає із контролю шунту на лівій стороні), тобто пропозиції, які формалізують стани, неявні з функції для того, щоб характеризувати властивості безпеки, - список небезпечних подій, яких потрібно уникнути, установлений, тут список, що буде згаданий пізніше, щоб вивести, через взаємозалежність, як пояснено надалі, суттєві резервні властивості системи 3, як позначено надалі. Таким чином, оскільки передбачається через взаємозалежність списку небезпечних подій резервних властивостей системи 3, небезпечні події, формалізовані глобальними станами FXj залізничної мережі та рухом потягу, та дозволом будьякому роботові 15 діяти тільки коли всі миттєві глобальні стани Fi, що випливає з його дії належать до додаткового набору з набору станів FXj у наборі доступних глобальних станів EGA. Для маневрової станції 1, небезпечними подіями на залізничній мережі є наступні: - два потяги є обличчям-до-обличчя або зіткнуться, - два потяги вдаряються боками, - напіввідчинене шунтування, - потяг, який є наздогнаний слідуючим потягом, - зсув вагонів, - сходження потягу з рельсів, - зіткнення з перешкодою. Резервні властивості роботів 15 будуть полягати в тому, щоб, наприклад, у першому випадку, утриматися від будь-якої команди на пристрої виводу (даних) 17, якщо система 3, щоб досягти цього, буде представлена єдиним станом Fi, ідентичному одному єдиному стану серед тут згаданих станів FXj, показуючи, що два потяги перебувають одночасно в протилежних напрямках на тому ж самому рельсовому путі. Кожен робот 15 повинен досягти кінцевого числа заключних станів які б не були події, що мотивували цей механізм. Інакше кажучи, кожен автоматичний модуль 15 є роботом кінцевого стану, математичне поняття, добре відоме фахівцям формальних мов. Інакше заявлене, автоматичні модулі 15 розміщені таким чином, що їхня дія може призвести тільки до кінцевого числа глобальних станів Fi. Функціонування системи реального часу 3 буде тепер роз'яснено. Спочатку, система 3 перебуває в "початковому" стабільному глобальному стані ESj. Для цього, стек маркування є паралельним таблиці 25, але тут, включений у пам'ять 16 роботів 15, містить визначені заздалегідь внутрішні змінні, індикативні їхньому початковому стану або їхній експлуатаційний статус, під час реалізації. Забезпечується, для функції ініціалізації FI організованої так, щоб взяти до уваги комбінацію станів змінної вводу-виводу 11, 17 та внутрішніх 11 змінних стеків маркування роботів 15 у початковий момент. Початковий стійкий глобальний стан ESj виходить з виконання функції ініціалізації FI. Доки немає ніякого випадку, що керівний модуль 13 зациклюється на собі у крок очікування (Фіг. 4). Протягом цього кроку 50, відповідно до Фіг. 3 й 4, будь-яка зміна стану TOR на вхідних лініях 11 виявляється блоком 12, що запам'ятовує відповідний випадок у стек очікування 22, наприкінці списку. Коли, протягом кроку 51, випадок en є найстарішим у стеку й знаходиться на самому початку списку, у правильний момент, що буде визначений пізніше, він управляється керівним модулем 13 так, що виконується відповідне завдання n. У наступному кроці 52, модуль 13 шукає у своїй таблиці, автоматичний модуль(і) 15, які повинні виконати таке завдання n, або принаймні розпочати його. Тоді це навантажує перший модуль 15 у блок обчислення 18. У кроці 53, інтерпретер 14 одночасно інтерпретує та виконує роботу робота 15 в блоку обчислення 18. Протягом такої роботи, робот 15 може: - мати стан внутрішніх змінних Іі, який управляє просуванням, у такий спосіб створюючи внутрішні події ір та одночасно запускаючи модуль маркування 19, - тестувати, як внутрішні так і зовнішні, змінні у вектору Fi, - емітувати команди до вихідних ліній 17 щоб командувати необхідними приводами 4, 5, - запускати затримки часу, зазначені затримки часу приводять до призначення подвійних значень до внутрішніх змінних, щоб використовуватися як індикатори часу затримки часу іншими роботами 15, - виконувати сигнальні або попереджуючі функції, - перевіряти, що резервні властивості супроводжуються, - виконувати обчислення, і т.д. Наприкінці роботи модуля 15 інтерпретер 14 запускає роботу модулю маркування 19 внутрішнього випадку. У цьому кроці 53, модуль маркування 19 систематично позиціює, якщо є присутність, внутрішні події ір у стеку 21 внутрішніх подій, але тільки попереджає керівний модуль 13 щодо факту, що є внутрішні події, які будуть оброблені наприкінці роботи робота 15, щоб обробити одночасно тільки один робот 15. При одержанні попередження від модуля 19, у кроці 54, модуль 13 перевіряє зміст стеку 21. Якщо стек 21 не порожній, завдання n у відповідності до зовнішнього випадку en не закінчено, і модуль 13 отримує, у кроці 55, найстаріший внутрішній випадок та повертається до вищезгаданого кроку 52, щоб, відповідно до зовнішніх подій, знайти у своїй таблиці 25, автоматичний модуль 15, який виконується, а потім запустити інтерпретер 14 для його одночасної обробки та виконання. 96601 12 Поки стек 21 містить внутрішній випадок, новий модуль 15 повинен розшукатися в таблиці 25 і повинен бути активізований у блоці 18. Роботи 15 призначені до завдання n є в такий спосіб потенційними вузлами діаграми станів en у відповідності зазначеному завданню n, зазначені вузли зв'язані між ними внутрішніми подіями ір, які є їхніми розгалуженнями. Рівень роботів 15 у такий спосіб згадується як рівень діаграми станів. Такі схеми приводять до вищеописаних доступних глобальних станів. Якщо стек 21 порожній, модуль 13, або рівень 14, досліджує, у таблиці 25, присутність іншого робота 15, для виконання обробки випадку, що відбувається, та, у такому випадку, завантаження цього в блок обчислення 18 та знову, приводить виконання кроку 52. Інакше, завдання n відносно події en є закінченим та керівний модуль 13 запускає модуль 20 зовнішніх подій маркування. Тоді модуль маркування 20 має стек 22 прогресу зовнішніх подій із видаленням з нього випадку en, що був тільки що оброблений і потім попереджає, взаємно, керуючий модуль 13 щодо факту, що наступний зовнішній випадок еn+1 стеку 22, якщо присутній, може бути прийнятий до розгляду. Тоді модуль 13 перевіряє у кроці 56, чи порожній стек 22 або ні та, - якщо він не порожній, модуль 13 повертається до кроку 51 щоб обробити наступний зовнішній випадок еn+1, - якщо він порожній, немає ніякого завдання n на виконання, модуль 13 повертається на його цикл очікування у кроці 50. Розуміється, що модуль 13 чекає протягом кінця триваючого завдання n перед запуском іншого завдання n+1, і тому виконання завдання n у відповідності будь-якому зовнішньому випадку en дозволяється тільки якщо немає ніякого завдання n-1 у відповідності іншому випадку еn-1, що вже виконується. Ніякий зовнішній випадок, що відбувається протягом тривалості виконання завдання, у такий спосіб не приймається до розгляду, що запобігає неконтрольованому розвитку миттєвого глобального вектора стану Fi протягом виконання завдання роботами 15. Усе трапляється нібито змінна часу була зовнішньою до системи 3, подібно до зовнішніх подій. Підсумовуючи, якщо відбувається свідчення небезпечної події, норми логічної та часової інтерпретації повинні бути дуже ясними. Ось чому система реального час 3 розділена на дві різних підсистеми реального часу, реалізована як стеком 21 так й 22, часи моніторингу tr та синхронізації Ті найчастіше протікають незалежно й тільки відповідають один щодо іншого, коли один з визначених заздалегідь стійких глобальних станів ESj досягнуто. Час tr не управляється інтерпретером 14, ні навіть рівнем діаграми станів. Навпроти, внутрішні події могли бути оброблені як зовнішні події й зроблені зовнішніми до системи 3. Тоді такі події поміщені в стек 22 замість стеку 21 керівним модулем 13 (за допомогою модулів маркування 19 й 20). Це могло, напри 13 клад, мати місце для внутрішніх змінних, які служать триваючими індикаторами затримки часу, коли вони повинні розпочинати завдання, відмінне від того, що відбувається. Це, у системі 3, є іншим видом "аутсорсингу" від часу Ті до часу tr. В останньому випадку, навіть затримки часу, синхронізовані моментами Ті також уникають контролю інтерпретеру 14 та роботів 15. Протягом кроку 53, модуль маркування 19 також передає до модуля 24 наявну інформацію, розвиток стану у цей час обробляється, тоді, у режимі реального часу, стани ір внутрішніми змінними призначаються модулем 15. Тоді модуль 24 генерує у пам'яті 16, у кожному моменті Ті, миттєвий глобальний стан Fi системи, та пам'яті 27 миттєвий функціональний глобальний стан Gi, у такий спосіб стаючи доступним для IHM 9. Коли модуль 13 одержує попередження від модуля 20, вимагаючи від нього взяти до розгляду наступний зовнішній випадок еn+1 та перевіряти схему Dn+1 як функцію Fi+1, це може перевірити, чи дійсно містить миттєвий глобальний стан Fi+1 стійкий глобальний стан ESj+1 та емітувати попередження, яке повинне бути відсутнє у такому миттєвому глобальному стані. Але тут, така перевірка відбувається тільки один раз протягом фази валідації після фази створення системи, що тепер буде пояснено. Відповідно до першого звичайного втілення, уже згаданого на початку документа, система, що дозволяє таку фазу валідації, відповідно до Фіг. 1 та 5, засоби залізничної мережі замінені, включаючи сепаратор 8, іншим комп'ютером моделювання 30, так, щоб систематично та автоматично тестувати всі розгалуження схем Dn. Комп'ютер 30, ілюстрований на Фіг. 1 та 3 та більше детально на Фіг. 5, може бути фізично ідентичним комп'ютеру 3. Це також включає вхідний пристрій 33 та лінії пристрою виводу (даних) 34, інтерфейс IHM 32, центральний елемент 31, що вміщує програмне забезпечення моделювання LS, пам'яті 36 та 37 паралельні пам'ятям 16 та 27, та робочої пам'яті MS програмного забезпечення LS. Пристрої вводу виводу (даних) 33-34 комп'ютера 30 пов'язані із пристроями вводу виводу (даних) 11-17 комп'ютерної системи 3 через комутуючий прилад 60 із двома позиціями R та S, як позначено на Фіг. 1, так, що у позиції R (реальній), комп'ютер 3 пов'язаний із сепаратором 8, та в позиції S (симульованій) комп'ютер 3 пов'язаний з комп'ютером 30. У позиції S, пристрої виводу (даних) 34 комп'ютера 30 зв'язані із вхідними пристроями 11 комп'ютера 3 та вхідні пристрої 33 комп'ютера 30 зв'язані із пристроями виводу (даних) 17 комп'ютера 3, так, щоб від програмного забезпечення моделювання LS комп'ютера 30 та через його пристрої виводу (даних) 34, вхідні пристрої 11 могли бути симульовані, начебто вони походили із сепаратора 8. Це є протилежним випадком для пристроїв виводу (даних) 17, відновлених вхідними пристроями 33 комп'ютера 30. 96601 14 Крім того, комп'ютери 3 та 30 зв'язані комп'ютерним з'єднанням 38 з швидкістю потоку, достатньою, щоб комп'ютер 30 міг блокувати та розблоковувати синхронізацію Ті годинників 23, ініціалізувати та читати розвиток миттєвих глобальних станів Fi та Gi пам'ятей 16 та 27 відповідно або в своїх пам'ятях 36 та 37. Пам'ять MS включає стеки Ro, So та St для запам'ятовування глобальних станів ESj та глобальних станів FXj. Ro дозволяє виконання моделювання завдання n та So містить J глобальних станів ESj, що буде перевірене, автоматично отримане простим програмним забезпеченням, визначеним для tri. St містить протестовані глобальні стани ESj. Пам'ять MS також містить стек Ео, що містить N значень, що здійснюють подвійні стани подій en та таблицю попередження E1, що буде зареєстровано. Крім того, програмне забезпечення LS повинно відповідати принаймні наступним умовам: - включати функції попередження, виведені з формалізації характеристик приводів, якими воно керує, - бути забезпеченим резервними властивостями, виведеними через взаємозалежність списку небезпечних подій. Щоб визначати функції попередження автоматичних модулів 15 з формалізації характеристик приводів, якими вони керують, умови формалізовані, будучи неявними з команди, що відбувається, та вони порівнюються зі станом мережі, наприклад, з огляду на те, що шунтування 4, яким маніпулюють, є лівим шунтуванням, функція попередження може включати перевірку, що відповідні стани ESj мережі та рух потягу, що забезпечується PC 2 та/або сенсорами 6, сумісні з лівою маніпуляцією, що відбувається. Таке перше втілення системи валідації потребує доповнення устаткування тестування, що вимагає відхилення від заключних експлуатаційних кондицій. Якщо автоматизми протестовані в їх заключному логічному контексті, вони не протестовані в їхньому заключному часовому контексті. Ось чому друге втілення із системи валідації, що показана на Фіг. 6, дійсно дозволяє встановлювати формальну валідацію та будучи, разом з цим, істотно простішим. Ця друга система валідації дійсно дозволяє здійснювати спосіб, цілком заснований на факті, що моделі, як визначено конструкторськими інструментами, є роботами 15 та у такий спосіб здатні бути безпосередньо інтерпретованими комп'ютером 3. Валідація включає перевірку чи задовольняються всі властивості безпеки в повному, матеріальному та насамперед часовому кінцевому експлуатаційному контексті. Таким чином, формальне свідчення безпеки в такий спосіб реалізується на моделях безпосередньо, які можуть, фактично, самі бути комп'ютерними транскрипціями, що можуть бути інтерпретованими, проектованої специфікації. 15 До цього: - Комп'ютер 30 містить комп'ютер 3 та вищеописане програмне забезпечення LS, розміщене так, щоб взаємодіяти з останнім у комп'ютері 30. Таким чином, набір даних, що міститься в комп'ютері 3, як тут вищеописане та показане на Фіг. 2, 3, 4, є також доступним для комп'ютера 30 та його програмного забезпечення LS, а комп'ютерне з'єднання 38 як між комп'ютерами 3 так і 30, так само як пам'ятями 36 та 37, не є необхідним. - Симуляційне програмне забезпечення LS симулює всі можливі зовнішні події на всіх можливих стійких глобальних станах, комп'ютерним шляхом, зі схем. Таким чином, у цьому втіленні системи валідації, пристрої вводу/виводу (даних) 33, 34 комп'ютера 30 не зобов'язані бути зв'язаними пристроями вводу/виводу (даних) 11, 17 комп'ютера 3. Комутуючий прилад 60 та лінії пристроїв вводу виводу (даних) 33 та 34 не присутні. Програмне забезпечення LS фактично контролює та керує комп'ютером 3, автоматично, більш особливо відповідно до способу, який зараз буде описаний. - Комп'ютер 30 має доступними всі дані та інформацію, присутню у комп'ютері 3 та необхідну щоб здійснити валідацію, що відбувається від них. З іншого боку, блокування/розблокування синхронізації годинника 23 не є необхідним, годинник реального часу 23 комп'ютера 3 також може забезпечити набір функцій годинника реального часу комп'ютера 30. - Інші вищеописані елементи комп'ютера 30 присутні. Таким чином, за допомогою цієї другої системи 30, робота системи 3 досягнута точно у таких же самих умовах матеріалу та часу протягом валідації системою 30 та протягом роботи. Додаткова перевага цього другого втілення полягає в тому, що є можливим, на комп'ютері 30, активувати крок за кроком виконуючий модуль, що неможливо здійснити на чітко запрограмованій системі реального часу 3. Тепер, яка б система не адаптувалась, для валідації системи 3, відповідно до Фіг. 7, моделювання, або контроль та керування комп'ютера 3, виконано програмним забезпеченням LS в комп'ютері 30 включає виконання наступних кроків: - крок 101: він отримує, з So, стійкий глобальний стан ESj (наприклад, починається з j = 1) від системи 3 та ініціалізує пам'яті Ro та 16 із цим першим стійким глобальним станом; - крок 102: він отримує з Ео зовнішній випадок en (наприклад n = 1 спочатку), це вводиться у стек 22, та запускає комп'ютер 3 розблоковуючи годинник 23; - крок 103: він моніторить послідовні миттєві глобальні стани Fi моментів Ті, поставлених модулем 24 та перевіряє, чи не є такі глобальні стани характеризуємі небезпечними подіями у порівнянні із глобальними станами FXj. У такому випадку, це зупиняє моделювання для виправлення; - інакше, крок 104: він порівнює послідовні миттєві глобальні стани Fi з усіма стійкими глобальними станами ESj стеку So та переходить до 96601 16 наступного кроку 105, як тільки одержує відповідність, тобто підсумовуючи стабільний глобальний стан ESj, крім випадку, якщо стек 21 не порожній; - в останньому випадку, він продовжує симуляцію, щоб досягти одного або більше інших підсумуючих глобальних станів ESj, крім випадку, якщо досягнутий стабільний глобальний стан є стійким глобальним станом, присутнім в стеку St, в якому разі, він переходить, однак, до кроку 105. Інакше заявлено, в останньому випадку, моделювання завдання n здійснюється, стійкий глобальний стан після стабілізованого глобального стану, доки досягнутий стійкий глобальний стан вже симульований та запам'ятований в St; - у кроці 105, якщо він не одержує стійкий глобальний стан наприкінці завдання, він записує попередження в таблицю E1 та переходить до кроку 106; - крок 106: він блокує годинник 23. Якщо всі події en Eo були симульовані, він переходить до кроку 107, інакше він виконує знову вищеописані кроки від кроку 101 симулюючи, у кроці 102, наступний зовнішній випадок еn+1; - крок 107: моделювання глобального стану ESj є повністю протестоване на всі N присутні зовнішні події en, це додає контент Ro (що містить симульований ESj) до стеку St видаляє його із стеку So; - крок 108: якщо стек So порожній, моделювання закінчене, він переходить до останнього вихідного кроку 109, на IHM 32, списків подій Ео та інших протестованих стійких глобальних станів St списку попереджень, отриманих з таблиці E1, інакше він знову виконує крок 101 та наступні, отримуючи наступний стійкий глобальний стан ESj+1 в So так, щоб продовжувати із моделюванням, стабільний глобальний стан стабільним глобальним станом та зовнішній випадок зовнішнім випадком, поки всі розгалуження всіх схем Dn не будуть закриті, тобто поки всі можливі комбінації подій та стабільні глобальні стани не були симульовані. Таким чином, повна валідація системи 3 може бути досягнута та, таким чином, формальне свідчення її експлуатаційної безпеки в короткому проміжку часу. Якщо була обрана перша система валідації, після моделювання, для здійснення, достатньо позиціювати комутуючий прилад 60 в позицію R, та тоді система 3 працює у тих же самих матеріальних та часових умовах, як протягом фази валідації. Тому немає ніякої різної матеріальної реалізації, здатної ввести втрату цілісності валідації щодо системи, яку приводять в дію. Подібно це відноситься до другої системи валідації. Щоб далі зменшувати складність системи або кількість її глобальних станів, моделювання можуть бути обмежені підмножинами часткових стійких глобальних станів Gi, автоматично виведених зі стійких глобальних станів ESj. Як заявлено тут вище, функції автоматичних модулів 15 можуть бути обмежені до таких, що дозволені експлуатаційним персоналом відповідно до норм, застосованих на маневрових станціях. 17 96601 18 19 96601 20 21 Комп’ютерна верстка Л. Литвиненко 96601 Підписне 22 Тираж 23 прим. Державна служба інтелектуальної власності України, вул. Урицького, 45, м. Київ, МСП, 03680, Україна ДП “Український інститут промислової власності”, вул. Глазунова, 1, м. Київ – 42, 01601