Формальный логический анализ корректности спецификаций сетевых SIP-протоколов
9
UAS startUas,
ackc?ack.!assertF Invited.reqc?bye.assertF Invited.brpc?by
Invited UAS.reqc!invite
Invited.
,
Confirmed Invited.irps?
Confirmed
eRsp.assertF
invSucc.!ackedF
ackc .
Confirmed.
?ack!ackedT
brpc?byeRsp!a
,
Bought Confirmed.
nvited.
ssertF
reqs!bye
Bought.ackc?ack!ackedT Bought .reqc?bye.brps!byeRsp,
Pr eEnded I
irps!invFail
reqc?bye.brps!byeRsp
Bought.brpc?byeRsp ,
Pr eEnded.!endUa
Confirmed.
Ended
Ended.
s
ackc?ack.!assertT
reqc?bye.brps!byeRsp
brpc?byeRs
Ended.
Ende
p!ass
d.
ertF.
Рис. 5.
Процессные выражения
UAS
3. Принципы перехода от процессного описания специфика-
ций к описанию на языке ПРОЛОГ и поиск некорректностей.
Переход от процессного описания SIP-спецификаций к описанию на
языке ПРОЛОГ включает следующие основные этапы:
• построение по процессному описанию агентов (спецификаций)
логической программы на языке ПРОЛОГ (от начального раздела до
раздела GOAL);
• построение по описанию на языке модальной логики раздела
GOAL;
• проверка свойства.
3.1.
Построение по процессному описанию агентов (SIP-специ-
фикаций) логической программы на языке ПРОЛОГ.
Принципы пе-
рехода от процессного описания к программе на языке ПРОЛОГ рас-
смотрим для одного процесса (агента), например для процесса
uac
(см. рис. 4). Он начинает выполняться после выполнения нити
start?startuac.
Поэтому в разделе
clauses
логической программы вво-
дим правило
uac([put(start,startuac)]):-thread([put(start,startuac)]),
означающее, что при истинности предиката
thread
([
put
(
start,startuac
)]),
аргументом которого является составной объект
put
(
start,startuac
),
соответствующий нити
start?startuac
,
становится истинным предикат
uac
([
put
(
start,startuac
)]), что интерпретируется как начало выполне-
