| Popis: |
Проведено порівняльний аналіз методів та засобів формальної верифікації, застосовуваних у процесі розроблення систем критичного призначення, зокрема – на етапі проєктування названого процесу. За результатами проведеного аналізу запропоновано і викладено комплексний підхід, що полягає у здійсненні контролю показників і функціональних, і нефункціональних характеристик названих систем вже на етапі проєктування процесу розроблення. Розглянуто модель подання функціональних характеристик розроблюваної системи у формальній специфікації, відмінними рисами якої є оперування трійками Гоара (C.A.R. Hoare) і відповідними аксіомами. За рахунок цього було досягнуто зменшення кількості рядків коду результуючої специфікації. Викладено запропонований метод синтезу формальних специфікацій функціональних характеристик розроблюваної системи, що будується на вищезазначеній моделі. У якості вихідних даних розглянуто блок-схему алгоритму, діаграму дій. За рахунок залучення виразних засобів темпоральної логіки дій Леслі Лемпорта (Leslie Lamport), а також алгоритмічної мови PlusCal, розроблений метод забезпечує механізм співставлення елементів аналітичного подання формальної специфікації функціональних характеристик із елементами подання рівня реалізації. Це відповідає центральній концепції Бертрана Мейера (Bertrand Meyer) – з точки зору безшовності сполучення застосовуваних виразних засобів, конструкцій. У якості сценаріїв предметної області, що реалізуються завдяки функціонуванню системи критичного призначення, опрацьовано сценарії космічної галузі, сценарії взаємодії учасників ринку електричної енергії на основі рольових моделей. Розглянуто складові рольової моделі ідентифікації учасників ринку електричної енергії з використанням формалізованого підходу, сценарії взаємодії учасників ринку електричної енергії на основі рольових моделей. Монографію призначено для аспірантів технічних напрямів, фахівців з аудиту та менеджменту в електроенергетиці, науковців та фахівців у галузі інформаційного обміну та функціонування ринків електричної енергії, розробників, діяльність яких пов’язана із проєктуванням програмно-алгоритмічного забезпечення комп’ютерних систем, зокрема систем критичного призначення, вбудованих систем. |
