On some class of mathematical models for static analysis of critical-mission asynchronous systems

• Main Authors: I.D. Perepelytsya, G.M. Zholtkevych, І.Д. Перепелиця, Г.М. Жолткевич, И.Д. Перепелица/ Г.Н. Жолткевич
• Format: Article in Journal/Newspaper
• Language: English
• Published: Харківський національний університет Повітряних Сил ім. І. Кожедуба 2011
• Subjects: Теоретичні основи розробки систем озброєння; УДК 004.414.23.042; critical-mission software; asynchronous software system; static analysis; live-lock; queue explosion; програмне забезпечення критичного призначення; асинхронні програмні системи; статичний аналіз; активний тупик; вибух черги; программное обеспечение критического назначения; асинхронные программные системы; статический анализ; активный тупик; взрыв очереди; Тупик
• Online Access: http://www.hups.mil.gov.ua/periodic-app/article/1879

A mathematical model of asynchronous software system is considered in the paper. This model bases on the notion abstract finite pre-machine which generalizes the notion abstract finite automaton. In contrast to generally accepted models the model proposed in the paper makes possible to specify more complex system behaviour than it is provided by finite automata models. Specifically, live-lock anomaly can be specified using the notion premachine. Authors adduce the criterion of live-lock existence and illustrate it by example. У статті розглянуто математичну модель асинхронних програмних систем. Ця модель спирається на поняття скінченої абстрактної перед-машини, яке узагальнює поняття абстрактного скінченого автомату. На відміну від загальноприйнятих моделей модель, запропонована в роботі, дозволяє описувати більш складну поведінку системи в порівнянні з моделями скінчених автоматів. Зокрема, аномалія «активний тупик» може бути промодельована в термінах скінченої перед-машини. Автори наводять критерій виникнення активного тупику та ілюструють його застосування на прикладі. В статье рассмотрена математическая модель асинхронных программных систем. Эта модель опирается на понятие абстрактной конечной пред-машины, которое обобщает понятие абстрактного конечного автомата. В отличие от общепринятых моделей модель, предложенная в работе, позволяет описывать более сложное поведение системы по сравнению с моделями конечных автоматов. В частности, аномалия «активный тупик» может быть промоделирована в терминах конечной пред-машины. Авторы приводят критерий возникновения активного тупика и иллюстрируют его применение на примере.