The paper presents the method of generating Labelled Transition Systems for passive agents in Alvis models. Alvis is the language designed for the modelling and formal verification of embedded systems. The key concept of Alvis is an agent which is any distinguished part of a considered system with defined identity persisting in the time. Alvis combines a graphical modelling of interconnections among agents with a high level programming language used for describing a behaviour of agents. The basic property of the Alvis Toolkit is the ability of a direct generation of a formal system description from an Alvis source code. The LTS graphs represent control flow related to Alvis code execution and they are the base for the formal model verification. Keywords: Alvis modeling language, embedded systems, microinstruction, formal verification

Радіоелектронні і комп'ютерні системи [Текст] // Радіоелектронні і комп'ютерні системи ; М-во освіти і науки України, Нац. аерокосм. ун-т ім. М. Є. Жуковського "Харк. авіац. ін-т" - Х. : ХАІ. — 2012.

• УДК // Вбудовані системи
• УДК // Комп’ютерні мови