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.

  Повний текст PDF - 537.678 Kb    Зміст випуску     Цитування публікації

  Якщо, ви не знайшли інформацію про автора(ів) публікації, маєте бажання виправити або відобразити більш докладну інформацію про науковців України запрошуємо заповнити "Анкету науковця"