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.
Ключові слова: critical-mission software, asynchronous software system, static analysis, live-lock, queue explosion
On some class of mathematical models for static analysis of critical-mission asynchronous systems,
Systems of Arms and Military Equipment,