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

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...

Full description

Bibliographic Details
Main Authors: I.D. Perepelytsya, G.M. Zholtkevych, І.Д. Перепелиця, Г.М. Жолткевич, И.Д. Перепелица/ Г.Н. Жолткевич
Format: Article in Journal/Newspaper
Language:English
Published: Харківський національний університет Повітряних Сил ім. І. Кожедуба 2011
Subjects:
Online Access:http://www.hups.mil.gov.ua/periodic-app/article/1879
Description
Summary: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. У статті розглянуто математичну модель асинхронних програмних систем. Ця модель спирається на поняття скінченої абстрактної перед-машини, яке узагальнює поняття абстрактного скінченого автомату. На відміну від загальноприйнятих моделей модель, запропонована в роботі, дозволяє описувати більш складну поведінку системи в порівнянні з моделями скінчених автоматів. Зокрема, аномалія «активний тупик» може бути промодельована в термінах скінченої перед-машини. Автори наводять критерій виникнення активного тупику та ілюструють його застосування на прикладі. В статье рассмотрена математическая модель асинхронных программных систем. Эта модель опирается на понятие абстрактной конечной пред-машины, которое обобщает понятие абстрактного конечного автомата. В отличие от общепринятых моделей модель, предложенная в работе, позволяет описывать более сложное поведение системы по сравнению с моделями конечных автоматов. В частности, аномалия «активный тупик» может быть промоделирована в терминах конечной пред-машины. Авторы приводят критерий возникновения активного тупика и иллюстрируют его применение на примере.