2006
Верификация автоматных программ средствами СРМ/ 70015
Виногшдое Р.А., Кузьмин E.B., Coma/we BA. <...> 4
Геометрические методы в задаче о минимальном проекторе
Невский M. <...> 16
Использование ТЕКСТУРНЫХ ПОКНННТЕЛЕЙ контрастности Hsofipaxcemm
B задаче НЕТОМЕШ‘ИЧВСКОЙ фОКУСИРОВКИ
Коротки“ А. <...> 36
Параметрический резонанс в одном уравнении m класса.
адиабатических осцилляторов
Hype В.Ш. <...> 61
Некоторые обобщения диаметра множества и задача [OJ-ma
Амин А.Б. <...> 13, M2 (2006) 4—15
\ [К DlQfiSffiF)
Верификация автоматных преграмм средствами CPN/Tools
Випигрцдов P.A., Кузьмин ТЁ. <...> Ярославский госудирстненнъш универгитст
150 000, Ярошавлъ, Советская, Ц
получена 15 толп 2006
Аннотация
В рибпти предлагали-си ‘ггхнппогия спецификации и. верификации ингомитнъц прптрамм Приди
Дятси обннружтшыс ошибки 11 дПТПМШП-ЮЙ модели гигтрмы управлении кофеваркой и вариант их
ПШЦНЬНЛОПИЯ‘ <...> Burma Tom, автоматный подход к 1|рограгммирившшю с точки зрения модели[МАНИ Н И}! <...> В (‘ч-иты' pa(‘EManuuam‘m тохпщшгия спецификации и верификации автоматных программ нос-грошпых по ипрархичг‘ской модели [(3i 7], которая осхповыиантся на применении метода model Checking. <...> Исследуется возможность спецификации (с точки зрения прогтптш и адекватности восприятии) структурных и семантических свойств гштомашпых программ с помощью темпоральной логики CTL [8, 9]. <...> Придуман и реши-венам механизм грнпигшции автоматных программ и CPN-Mlmmm Предлагаемая
тохпшлопш ггюпификшпаи и верификации автоматных программ, построив—(пых по иерархической модным, опробшишп на примере сигтнмы ущлашшпин кпфеваркой ГЛ 15]. <...> Конечноггь системы переходов означаещ что система имеет конечное числи Состояний. <...> Днище в рамках структуры Крипкс с ишюиьзонпнпем 51'stна тсмипральной логики гггецнфицируются свойства программной модели, истинность котпрых для этой
Be ификация автоматных п югра :M (: ечствдьми CPNf‘Tuuls
7 _I_ _‚ 7 rмодели затем и проверяется, С исмпльзованинм таких пристых объектов как конечная система переходов и формулы темппршшной логики, возможно <...>