УДК 621.391.1: 681.883.3
Виявлення і вимірювання швидкості ходу морських суден по зображенню їх спутного сліду / Горбань І.І., Целищев І.Ю. // Математичні машини і системи. - 2011. - № 1. - С. 9 - 19.
На основі дослідження зображень рухомих морських суден, що отримані за допомогою аерокосмічних систем спостереження, розроблені математичні моделі їх спутних слідів. Для різних моделей спутних слідів та завад синтезовано оптимальні за критерієм максимуму функції вірогідності алгоритми виявлення морських суден та вимірювання напрямку і швидкості їх ходу. Запропоновано квазіоптимальний алгоритм адаптивної багатоканальної обробки зображень, що забезпечує виявлення суден та вимірювання параметрів їх руху. Показано, що завадостійкість системи квазіоптимальної обробки зображень зростає з підвищенням швидкості руху судна. Іл.: 8. Бібліогр.: 4 назв.
УДК 621.391.1: 681.883.3
Обнаружение и измерение скорости хода морских суден по изображению их спутного следа / Горбань И.И., Целищев И.Ю. // Математические машины и системы. - 2011. - № 1. - С. 9 - 19.
На основе анализа изображений движущихся морских суден, полученных с помощью аэрокосмических систем наблюдения, разработаны математические модели их спутных следов. Для разных моделей спутных следов и помех синтезированы оптимальные по критерию максимума функции правдоподобия алгоритмы обнаружения морских суден и измерения направления и скорости их хода. Предложен квазиоптимальный алгоритм адаптивной многоканальной обработки изображений, обеспечивающей обнаружение суден и измерение параметров их движения. Показано, что помехоустойчивость системы квазиоптимальной обработки изображений возрастает с увеличением скорости хода судна. Ил.: 8. Библиогр.: 4 назв.
УДК 681.513.7; 681.5.013
Застосування методу контрольованого збурення для модифікації нейроконтролерів у реальному часі / Дзюба Д.O., Чернодуб А.М. // Математичні машини і системи. - 2011. - № 1. - С. 20 - 28.
Запропоновано новий метод навчання нейронних мереж керуванню динамічними об'єктами, який базується на оцінці локальних значень якобіану положення об'єкта по керуванню за рахунок використання малих збурень управління, що прикладається до об'єкта. Метод не вимагає апріорної інформації про об'єкт керування і може використовуватись для адаптивного керування об'єктами різної природи. Експерименти з використанням запропонованого методу для навчання рекурентних нейромереж у системах керування різними об'єктами демонструють переваги такого нейрокерування над стандартним PID-керуванням. Іл.: 9. Бібліогр.: 17 назв.
УДК 681.513.7; 681.5.013
Применение метода контролируемого возмущения для модификации нейроконтроллеров в реальном времени / Дзюба Д.А., Чернодуб А.Н. // Математические машины и системы. - 2011. - № 1. - С. 20 - 28.
Предложен новый метод обучения нейронных сетей управлению динамическими объектами, базирующийся на оценке локальных значений якобиана положения объекта по управлению за счет использования малых возмущений прикладываемого управления. Метод не требует наличия априорной информации об управляемом объекте и может использоваться для адаптивного управления объектами различной природы. Эксперименты по использованию предложенного метода для обучения рекуррентных нейросетей в системах управления различными объектами демонстрируют преимущества такого нейроуправления над стандартным PID-управлением. Ил.: 9. Библиогр.: 17 назв.
УДК 519.2:612.822
Статистичне моделювання дендритів нейронів / Бондаренко Я.С., Турчин В.М. // Математичні машини і системи. - 2011. - № 1. - С. 29 - 38.
У роботі запропоновано загальну ймовірнісну модель дендритів нейронів. Розроблено алгоритм моделювання дендрита, складниками якого є алгоритми моделювання ланки сегмента, моделювання сегмента без піддерев, моделювання сегмента з піддеревами, моделювання піддерева -го рівня. Робота алгоритму моделювання дендритів нейронів апробована і проілюстрована моделюванням дендритів Пуркін'є клітин кори мозочка морської свинки. Іл.: 4. Бібліогр.: 11 назв.
УДК 519.2:612.822
Статистическое моделирование дендритов нейронов / Бондаренко Я.С., Турчин В.Н. // Математические машины и системы. - 2011. - № 1. - С. 29 - 38.
В работе предложена вероятностная модель дендритов нейронов. Разработан алгоритм моделирования дендрита, состоящий из алгоритмов моделирования звена сегмента, моделирования сегмента без поддеревьев, моделирования сегмента с поддеревьями, моделирования поддерева -го уровня. Работа алгоритма моделирования дендритов нейронов проиллюстрирована моделированием дендритов Пуркинье клеток коры мозжечка морской свинки. Ил.: 4. Библиогр.: 11 назв.
УДК 57.001
Біометричні технології ідентифікації людини. Огляд системи / Мороз А.О. // Математичні машини і системи. - 2011. - № 1. - С. 39 - 45.
У статті розглянуті біометричні методи ідентифікації людини, їх розвиток та сучасне застосування. Наведені приклади розвитку біометричних систем та їх роль у світі інформаційних технологій. Бібліогр.: 12 назв.
УДК 57.001
Биотехнические технологии идентификации человека. Обзор системы / Мороз А.А. // Математические машины и системы. - 2011. - № 1. - С. 39 - 45.
В статье рассмотрены биометрические методы идентификации человека, их развитие и применение в современном мире. Приведены примеры развития биометрических технологий и их роль в мире информационных технологий. Библиогр.: 12 назв.
НОВІ ІНФОРМАЦІЙНІ І ТЕЛЕКОМУНІКАЦІЙНІ ТЕХНОЛОГІЇ
УДК 314:004.04
Рішення демографічних проблем за допомогою розподілених інформаційних технологій / Сапатий П.С., Сугісака М. // Математичні машини і системи. - 2011. - № 1. - С. 46 - 60.
У роботі розглянуто високорівневу технологію розподіленого керування та контролю, яка спроможна вирішувати складні нелокальні задачі по підтримці старіючого населення та його подальшій участі в розвитку суспільства. Запропонований підхід об'єднує фізичний та віртуальний світи в високоорганізоване розподілене середовище, що охоплює «розумний» дім, «розумне» місто аж до «розумного» суспільства та світу. Цей об'єднаний світ може эфективно оброблятись і керуватись за допомогою паралельного просторового автомата, що динамічно покриває та інтегрує існуючі людські і роботичні ресурси для цілеспрямованих сумісних дій та рішень. Іл.: 9. Бібліогр.: 35 назв.
УДК 314:004.04
Решение демографических проблем с помощью распределенных информационных технологий / Сапатый П.С., Сугисака М. // Математические машины и системы. - 2011. - № 1. - С. 46 - 60.
В работе рассматривается высокоуровневая технология распределенного управления и контроля, способная решать сложные нелокальные задачи по поддержке стареющего населения и его дальнейшему участию в развитии общества. Изложенный подход объединяет физический и виртуальный миры в единую высокоорганизованную распределенную среду, охватывающую «умный» дом, «умный» город, вплоть до «умного» общества и мира. Этот объединенный мир может эффективно обрабатываться и управляться с помощью параллельного пространственного автомата, динамически покрывающего и интегрирующего имеющиеся человеческие и роботические ресурсы для целенаправленных совместных действий и решений. Ил.: 9. Библиогр.: 35 назв.
УДК 681.3
Інтелектуалізований інтерфейс користувача інформаційно-пошукової системи у задачі пошуку за ключовим словом («зразком») з упереджувальною підказкою / Кузьменко Г.Є., Литвинов В.А., Майстренко С.Я., Оксанич І.М. // Математичні машини і системи. - 2011. - № 1. - С. 61 - 71.
Розглядається типовий інтерфейс користувача у задачі пошуку за зразком (ключовим словом) з упереджувальною підказкою. Пропонуються математичні моделі оцінки трудомісткості варіантів інтерфейсу з покроковою та прицільною підказкою. Наводяться результати імітаційного моделювання процесів формування підказки. Табл.: 10. Іл.: 3. Бібліогр.: 7 назв.
УДК 681.3
Интеллектуализованный интерфейс пользователя информационно-поисковой системы в задаче поиска по ключевому слову («образцу») с упреждающей подсказкой / Кузьменко Г.Е., Литвинов В.А., Майстренко С.Я., Оксанич И.Н. // Математические машины и системы. - 2011. - № 1. - С. 61 - 71.
Рассматривается типовой интерфейс пользователя в задаче поиска по образцу (ключевому слову) с упреждающей подсказкой. Предлагаются математические модели оценки трудоемкости вариантов интерфейса с пошаговой и прицельной подсказкой. Приводятся результаты имитационного моделирования процессов формирования подсказки. Табл.: 10. Ил.: 3. Библиогр.: 7 назв.
УДК 004.9:504
Розробка архітектури кросплатформних розподілених систем підтримки прийняття рішень, основаних на математичних моделях / Євдін Є.О. // Математичні машини і системи. - 2011. - № 1. - С. 72 - 81.
Представлено архітектуру системи підтримки прийняття рішень, основаної на математичних моделях. Описані структури даних, що дозволяють уніфікувати обмін даними, стандартизувати процес інтеграції моделей та поєднання їх у ланцюги. Моделі організовані у формі плагинів, які містять усю залежну від них функціональність. Архітектура системи передбачає наявність трьох компонентів, кожен з яких може бути розташований на окремому комп'ютері в мережі: управляючий сервер для забезпечення взаємодії інших компонентів, клієнтська частина з графічним інтерфейсом для збору та візуалізації даних, обчислювач для запуску на виконання математичних моделей та сервери баз даних. Іл.: 4. Бібліогр.: 12 назв.
УДК 004.9:504
Разработка архитектуры кроссплатформенных распределённых систем поддержки принятия решений, основанных на математических моделях / Евдин Е.А. // Математические машины и системы. - 2011. - № 1. - С. 72 - 81.
Представлена архитектура системы поддержки принятия решений, основанной на математических моделях. Описаны структуры данных, которые позволяют унифицировать обмен данными, стандартизировать процесс интеграции моделей и объединения их в цепочки. Модели организованы в форме плагинов, которые содержат всю зависимую от них функциональность. Архитектура системы предполагает наличие трёх компонентов, каждый из которых может исполняться на отдельном компьютере в сети: управляющий сервер, обеспечивающий взаимодействие остальных компонентов, клиентская часть с графическим интерфейсом для сбора и визуализации данных, вычислитель для запуска математических моделей на исполнение и серверы баз данных. Ил.: 4. Библиогр.: 12 назв.
МОДЕЛЮВАННЯ І УПРАВЛІННЯ ВЕЛИКИМИ СИСТЕМАМИ
УДК 004.89
Невизначеність і причинно-наслідковий принцип оптимізації систем пожежного моніторингу / Землянський О.М., Литвинов В.В., Снитюк В.Є. // Математичні машини і системи. - 2011. - № 1. - С. 82 - 89.
У статті розглянуто проблему проектування і оптимізації систем пожежного моніторингу. Запропоновано причинно-наслідковий принцип оптимізації таких систем, у відповідності з яким їх надійність та ефективність повинні залежати від кількості можливих жертв і масштабу можливих збитків. Розроблено елементи технології прийняття рішень при проектуванні систем пожежного моніторингу з використанням такого принципу, а також результатів моделювання, одержаних на основі застосування композиції методів «м'яких» обчислень. Іл.: 5. Бібліогр.: 10 назв.
УДК 004.89
Неопределенность и причинно-следственный принцип оптимизации систем пожарного мониторинга / Землянский А.Н., Литвинов В.В., Снитюк В.Е. // Математические машины и системы. - 2011. - № 1. - С. 82 - 89.
В статье рассмотрена проблема проектирования и оптимизации систем пожарного мониторинга. Предложен причинно-следственный принцип оптимизации таких систем, в соответствии с которым их надежность и эффективность должны зависеть от количества возможных жертв и масштаба материального ущерба. Разработаны элементы технологии принятия решений при проектировании систем пожарного мониторинга с использованием такого принципа, а также результатов моделирования, полученных на основе применения композиции методов «мягких» вычислений. Ил.: 5. Библиогр.: 10 назв.
УДК 004.9:504:519.6
Використання паралельних обчислень у метеорологічній моделі WRF / Ковалець І.В., Гузій О.М. // Математичні машини і системи. - 2011. - № 1. - С. 90 - 95.
Досліджені можливості застосування алгоритмів розпаралелення для підвищення швидкодії метеорологічної моделі WRF. Теоретично й експериментально досліджені можливості алгоритму розпаралелення обчислень по областях. Представлена автоматична система паралельних розрахунків незалежних метеорологічних сценаріїв. Іл.: 3. Бібліогр.: 4 назв.
УДК 004.9:504:519.6
Использование параллельных вычислений в метеорологической модели WRF / Ковалец И.В., Гузий А.М. // Математические машины и системы. - 2011. - № 1. - С. 90 - 95.
Исследованы возможности применения алгоритмов распараллеливания для повышения быстродействия метеорологической модели WRF. Теоретически и экспериментально исследованы возможности алгоритма распараллеливания вычислений по областям. Представлена автоматическая система параллельного расчета независимых метеорологических сценариев. Ил.: 3. Библиогр.: 4 назв.
УДК 621.9:001.8
Формалізація постановки багатофакторного експериментального дослідження / Радченко С.Г. // Математичні машини і системи. - 2011. - № 1. - С. 96 - 102.
Розглянуто постановку експериментального дослідження із загальносистемних позицій. Уперше сформульовані вимоги до стійких (робастних) планів експериментів, стійких структур багатофакторних статистичних моделей і стійкості коефіцієнтів моделей. Наведено приклади успішного використання розробленого методу коректного рішення багатофакторних регресійних задач. Бібліогр.: 9 назв.
УДК 621.9:001.8
Формализация постановки многофакторного экспериментального исследования / Радченко С.Г. // Математические машины и системы. - 2011. - № 1. - С. 96 - 102.
Рассмотрена постановка экспериментального исследования с общесистемных позиций. Впервые сформулированы требования к устойчивым (робастным) планам экспериментов, устойчивым структурам многофакторных статистических моделей и устойчивости коэффициентов моделей. Приведены примеры успешного использования разработанного метода корректного решения многофакторных регрессионных задач. Библиогр.: 9 назв.
УДК 681.3;504.75;004.75
Перший Кримський експериментальний обчислювальний Grid|-ресурс: створення і перші результати випробувань і експлуатації / Храмов В.В., Судаков О.О., Кононов М.В. // Математичні машини і системи. - 2011. - № 1. - С. 103 - 111.
У статті представлено специфіку основних проблем застосування комп'ютерного моделювання в гуманітарних і екологічних дослідженнях. Описані переваги використання Grid-кластера для паралельної обробки інформації у вищевказаних галузях. Обґрунтовується вибір стратегії для створення експериментального обчислювального Grid-кластера. Експериментально доводиться, що вибраний підхід з застосуванням кластерних технологій та методів паралельної обробки інформації є ефективним для цих задач. Наведено особливості побудови і перші результати використання обчислювального Grid-кластера на основі запропонованої стратегії. Табл.: 3. Іл.: 4. Бібліогр.: 19 назв.
УДК 681.3;504.75;004.75
Первый Крымский экспериментальный вычислительный Grid-ресурс: создание и первые результаты испытаний и эксплуатации / Храмов В.В., Судаков O.О., Кононов М.В. // Математические машины и системы. - 2011. - № 1. - С. 103 - 111.
В статье представлена специфика основных проблем применения компьютерного моделирования в гуманитарных и экологических исследованиях. Описаны преимущества использования Grid-кластера для параллельной обработки информации в вышеуказанных отраслях. Обосновывается выбор стратегии для создания экспериментального вычислительного Grid--кластера. Экспериментально доказывается, что предложенный подход с применением кластерных технологий и методов параллельной обработки информации является эффективным для задач данного класса. Приведены особенности построения и первые результаты использования вычислительного Grid-кластера на основе предложенной стратегии. Табл.: 3. Ил.: 4. Библиогр.: 19 назв.
УДК 531.37
Комбінований метод розпізнавання причини виникнення захворювання / Шкуліпа О.В., Рубльов Б.В., Шейман Б.С. // Математичні машини і системи. - 2011. - № 1. - С. 112 - 119.
У роботі наведено підходи до побудови алгоритму розпізнавання причини виникнення захворювання. Запропоновано комбінований метод для визначення причини виникнення захворювання у хворого. Розглянуто роботу алгоритмів, що були використані, та їх покрокове застосування на практиці. Проведено оцінку можливості використання комбінованого методу на практиці. Табл.: 4. Іл.: 3. Бібліогр.: 5 назв.
УДК 531.37
Комбинированный метод распознавания причины возникновения болезни / Шкулипа Е.В., Рублев Б.В., Шейман Б.С. // Математические машины и системы. - 2011. - № 1. - С. 112 - 119.
В работе представлены подходы к распознаванию причины возникновения болезни. Представлен комбинированный метод для определения причины возникновения болезни у больного. Продемонстрирована работа алгоритмов, которые были использованы, и их пошаговое применение на практике. Проведена оценка возможности ее использования для распознавания причины возникновения болезни. Табл.: 4. Ил.: 3. Библиогр.: 5 назв.
УДК 539.172:543.522
Задача визначення поточного ризику об'єкта підвищеної небезпеки / Бєгун В.В. // Математичні машини і системи. - 2011. - № 1. - С. 120 - 126.
Пропонується рішення задачі визначення поточного ризику об'єкта підвищеної небезпеки за результатами моніторингу (перевірки) залежно від стану систем безпеки й устаткування підприємства, стану підготовки персоналу, стану технологічної документації (процедур), інших зовнішніх і внутрішніх факторів на основі попередньо розроблених імовірнісних моделей. Бібліогр.: 11 назв.
УДК 539.172:543.522
Задача определения текущего риска объекта повышенной опасности / Бегун В.В. // Математические машины и системы. - 2011. - № 1. - С. 120 - 126.
Предлагается решение задачи определения текущего риска объекта повышенной опасности по результатам мониторинга (проверки) в зависимости от состояния систем безопасности и оборудования предприятия, состояния подготовки персонала, состояния технологической документации (процедур), других внешних и внутренних факторов на основе предварительно разработанных вероятностных моделей. Библиогр.: 11 назв.
УДК 621.396
Імітаційна модель для визначення сприйняття якості обслуговування абонентів IP-телефонії / Стрюк О.Ю., Янсонс Я.В. // Математичні машини і системи. - 2011. - № 1. - С. 127 - 134.
Проведений аналіз сприйняття якості обслуговування (PQoS) як цільової функції задачі мережевого керування. Запропонована імітаційна модель для визначення значень PQoS. Проведене експериментальне дослідження гіпотези IQX для кодеку мови SPEEX. Табл.: 2. Іл.: 3. Бібліогр.: 20 назв.
УДК 621.396
Имитационная модель для определения восприятия качества обслуживания абонентов IP-телефонии / Стрюк А.Ю., Янсонс Я.В. // Математические машины и системы. - 2011. - № 1. - С. 127 - 134.
Проведен анализ восприятия качества обслуживания (PQoS) как целевой функции задачи сетевого управления. Предложена имитационная модель для определения значений PQoS. Проведено экспериментальное исследование гипотезы IQX для кодека речи SPEEX. Табл.: 2. Ил.: 3. Библиогр.: 20 назв.
УДК 519.85
Оцінювання параметрів рівняння регресії за нечіткими вихідними даними / О.В. Сєрая, Т.І. Каткова // Математичні машини і системи. - 2011. - № 1. - С. 135 - 140.
Розглянуто технологію оцінювання параметрів рівняння регресії для випадку, коли вихідні дані - нечіткі числа з відомими функціями приналежності. Запропоновано метод розрахунку чітких значень шуканих оцінок, заснований на відшуканні чіткого рішення нечіткої системи лінійних алгебраїчних рівнянь. Бібліогр.: 4 назв.
УДК 519.85
Оценивание параметров уравнения регрессии по нечетким исходным данным / О.В. Серая, Т.И. Каткова // Математические машины и системы. - 2011. - № 1. - С. 135 - 140.
Рассмотрена технология оценивания параметров уравнения регрессии для случая, когда исходные данные - нечеткие числа с известными функциями принадлежности. Предложен метод расчета четких значений искомых оценок, основанный на отыскании четкого решения нечеткой системы линейных алгебраических уравнений. Библиогр.: 4 назв.
ЯКІСТЬ, НАДІЙНІСТЬ І СЕРТИФІКАЦІЯ ОБЧИСЛЮВАЛЬНОЇ ТЕХНІКИ І ПРОГРАМНОГО ЗАБЕЗПЕЧЕННЯ
УДК 621.3.019:658.562
Експериментальна оцінка надійності виробів в умовах малого числа відмов / Стрельніков П.В. // Математичні машини і системи. - 2011. - № 1. - С. 141 - 146.
Представлено результати аналізу існуючих методів і методик експериментальної оцінки показників надійності. Розглядаються методики оцінки показників надійності в умовах малої статистики відмов на основі використання двопараметричних імовірнісно-фізичних моделей надійності (дифузійних розподілів). Табл.: 1. Іл.: 1. Бібліогр.: 5 назв.
УДК 621.3.019:658.562
Экспериментальная оценка надежности изделий в условиях малого числа отказов / Стрельников П.В. // Математические машины и системы. - 2011. - № 1. - С. 141 - 146.
Представлены результаты анализа существующих методов и методик экспериментальной оценки показателей надежности. Рассматриваются методики оценки показателей надежности в условиях малой статистики отказов на основе использования двухпараметрических вероятностно-физических моделей надежности (диффузионных распределений). Табл.: 1. Ил.: 1. Библиогр.: 5назв.
ДИСКУСІЙНІ ПОВІДОМЛЕННЯ
УДК 681.3
Біогенетичний закон Геккеля і його роль у виявленні механізму ретрансляції природних законів у процес створення та еволюціонування обчислювальної техніки. Ч. 3 / Брюхович Є.І. // Математичні машини і системи. - 2011. - № 1. - С. 147 - 153.
Отримано відповідь на питання, як людина створює і еволюціонує обчислювальну техніку за природними законами. Відповідь міститься в механізмі дії відомої центральної догми молекулярної біології (ЦДМБ), яка лежить в основі біогенетичного закону Геккеля і послужила новим обґрунтуванням справедливості тверджень цього закону, за яким відбувається коротке і швидке повторення (рекапітуляція) індивідуальним розвитком особи (онтогенезом) найважливіших етапів еволюції виду (філогенезу). Рекапітуляція обумовлена тим, що, відповідно до центральної догми молекулярної біології, ЗНК знімає копію генетичної інформації, що міститься в ДНК, не руйнуючи оригінал, внаслідок чого в ДНК відбувається послідовне нашарування генетичної інформації протягом усього філогенезу виду. Зроблено висновок, що при створенні і еволюціонуванні обчислювальної техніки людина, сама того не усвідомлюючи, рекапітулює філогенез з Homo sapiens в онтогенез Computer sapiens. Бібліогр.: 9 назв.
УДК 681.3
Биогенетический закон Геккеля и его роль в выявлении механизма ретрансляции естественных законов в процесс создания и эволюционирования вычислительной техники. Ч. 3 / Брюхович Е.И. // Математические машины и системы. - 2011. - № 1. - С. 147 - 153.
Получен ответ на вопрос, как человек создает и эволюционирует вычислительную технику по естественным законам. Ответ содержится в механизме действия известной центральной догмы молекулярной биологии (ЦДМБ), которая лежит в основе биогенетического закона Геккеля и послужила новым обоснованием справедливости утверждений этого закона, по которому происходит краткое и быстрое повторение (рекапитуляция) индивидуальным развитием особи (онтогенезом) важнейших этапов эволюции вида (филогенеза). Рекапитуляция обусловлена тем, что, в соответствии с центральной догмой молекулярной биологии, РНК снимает копию генетической информации, содержащейся в ДНК, не разрушая оригинал, вследствие чего в ДНК происходит последовательное наслоение генетической информации в течение всего филогенеза вида. Сделан вывод, что, создавая и эволюционируя вычислительную технику, человек, не осознавая того сам, рекапитулирует филогенез Homo sapiens в онтогенез Computer sapiens. Библиогр.: 9 назв.
УДК 004.052
Наскільки формальні формальні методи? / Тарасюк О.М., Горбенко А.В., Харченко В.С. // Математичні машини і системи. - 2011. - № 1. - С. 154 - 167.
У статті аналізуються проблеми, пов'язані з розвитком та застосуванням формальних методів під час створення й верифікації програмного забезпечення та комп'ютерних систем. Дається класифікація інваріантів. Уточнюються поняття й процедура синтезу системи інваріантів та її оптимізація за певними критеріями. Розглянуто моделі життєвого циклу за умов використання формальних методів Event-B та Model Checking, їх особливості та обмеження. Сформульовано напрямки подальших досліджень у цій області. Іл.: 3. Бібліогр.: 24 назв.
УДК 004.052
Насколько формальны формальные методы? / Тарасюк О.М., Горбенко А.В., Харченко В.С. // Математические машины и системы. - 2011. - № 1. - С. 154 - 167.
В статье анализируются проблемы, связанные с развитием и внедрением формальных методов при разработке и верификации программного обеспечения и компьютерных систем. Дается классификация инвариантов. Уточняются понятие и процедура синтеза системы инвариантов и ее оптимизации по некоторым критериям. Предлагаются модели жизненного цикла программного обеспечения при использовании формальных методов Event-B и Model Checking. Анализируются их особенности и ограничения. Формулируются направления дальнейших исследований в этой области. Ил.: 3. Библиогр.: 24 назв.
РЕЦЕНЗІЇ
Нові фундаментальні можливості математичних машин і систем / А.О. Морозов // Математичні машини і системи. - 2011. - № 1. - С. 168 - 169.
Рецензія на книгу Синькова М.В., Бояринової Ю.Є., Калиновського Я.А. "Гіперкомплексні числові системи. Основи теорії. Застосування".
Новые фундаментальные возможности математических машин и систем / А.А. Морозов // Математические машины и системы. - 2011. - № 1. - С. 168 - 169.
Рецензия на книгу Синькова М.В., Бояриновой Ю.Е., Калиновского Я.А. "Гиперкомплексные числовые системы. Основы теории. Применения".
