Cybernetics And Systems Analysis
International Theoretical Science
Journal
Abstract. The paper describes a new generator of symbolic traces, which is designed for the latest version of insertion modeling system. The main characteristics of the generator is the use of graphic representations of the description of multilevel models, division of local descriptions and consequence relation, the possibility of configuration to different search strategies, and application of a new predicate transformer, which admits generality quantifiers with relaxed constraints with respect to the previous versions.
Keywords: verification, insertion modeling, UCM.
Летичевский Александр Адольфович,
академик НАН Украины, профессор, заведующий отделом Института кибернетики им. В.М. Глушкова НАН Украины, Киев,
e-mail: let@cyfra.net; let@iss.org.ua; aaletichevsky78@gmail.com.
Летичевский Александр Александрович,
кандидат физ.-мат. наук, старший научный сотрудник Института кибернетики им. В.М. Глушкова НАН Украины, Киев,
e-mail: lit@iss.org.ua.
Песчаненко Владимир Сергеевич,
кандидат физ.-мат. наук, доцент Херсонского государственного университета
e-mail: lvladim@ksu.ks.ua.
Губа Антон Андреевич,
младший научный сотрудник Института кибернетики им. В.М. Глушкова НАН Украины, Киев,
e-mail: anton.huba@iss.org.ua.
