Форум АСУ в Україні http://asu.in.ua/ |
|
Model checking - метод верифікації ПЗ http://asu.in.ua/viewtopic.php?f=235&t=859 |
Сторінка 2 з 2 |
Автор: | san [ 12 жовтня 2014, 18:13 ] |
Тема повідомлення: | Re: Model checking - метод верифікації ПЗ |
Model Checking для CTL AXϕ выполняется в состоянии s , если формула ϕ выполняется во всех состояниях, непосредственно следующих за s ; EXϕ выполняется в состоянии s , если формула ϕ выполняется хотя бы в одном состоянии, непосредственно следующем за s ; AFϕ (неизбежно ϕ ) выполняется в состоянии s , если на всех путях, начинающихся из состояния s , формула ϕ когда-нибудь выполнится; EFϕ (возможно ϕ ) выполняется в состоянии s , если из этого состояния существует путь, на котором формула ϕ когда-нибудь выполнится; AGϕ (глобально ϕ ) выполняется в состоянии s , если на всех путях, начинающихся из состояния s , во всех состояниях этих путей формула ϕ выполняется; EGϕ выполняется в состоянии s , если существует путь из s , во всех состояниях которого формула ϕ выполняется; A(ϕ1Uϕ2 ) выполняется в состоянии s , если на всех путях, начинающихся в s , когда-нибудь в будущем выполнится формула ϕ2 , а до этого во всех состояниях этих путей выполняется формула ϕ1 ; E (ϕ1Uϕ2) выполняется в состоянии s , если из s существует путь, на котором когда-нибудь в будущем выполнится ϕ2 , а до этого во всех состояниях этого пути выполняется ϕ1 . |
Сторінка 2 з 2 | Часовий пояс UTC + 2 годин [ DST ] |
Powered by phpBB © 2000, 2002, 2005, 2007 phpBB Group http://www.phpbb.com/ |