Skip to content

Commit 2b48e0c

Browse files
5HT5HT
committed
на почитати
1 parent a7b6a37 commit 2b48e0c

4 files changed

Lines changed: 337 additions & 0 deletions

File tree

‎priv/itu-z.120.pdf‎

1.32 MB
Binary file not shown.

‎priv/msc-z.120.pdf‎

287 KB
Binary file not shown.

‎priv/msc-z.120.tex‎

Lines changed: 207 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,207 @@
1+
\documentclass[11pt,a4paper]{article}
2+
\usepackage[utf8]{inputenc}
3+
\usepackage[T2A]{fontenc}
4+
\usepackage[ukrainian,english]{babel}
5+
\usepackage{amsmath}
6+
\usepackage{amssymb}
7+
\usepackage{listings}
8+
\usepackage{graphicx}
9+
\usepackage{hyperref}
10+
\usepackage{geometry}
11+
\geometry{margin=2.5cm}
12+
13+
\title{Адаптація акторної архітектури чат-системи до нотації Message Sequence Chart (ITU-T Z.120)}
14+
\author{Грок (на основі аналізу репозиторію synrc/chat)}
15+
\date{\today}
16+
17+
\begin{document}
18+
19+
\maketitle
20+
21+
\begin{abstract}
22+
У цьому документі проводиться аналіз мови опису архітектури ядра чат-системи з репозиторію \texttt{synrc/chat} (файл \texttt{ARCH-KERNEL-MAPPINGS.md}), яка базується на алгебраїчних типах, морфізмах та чіткому розділенні \texttt{Action}, \texttt{Event}, \texttt{Observation} та \texttt{Predicate}.
23+
24+
Ми адаптуємо цю модель до стандартизованої нотації \textbf{Message Sequence Chart} (MSC) за рекомендацією ITU-T Z.120. Пропонується відповідність між елементами kernel (Principal, Session, Post, Mutate, Seen(EventObs(...)) тощо) та конструкціями MSC (instances, messages, actions, inline expressions alt/par/opt, conditions, HMSC).
25+
26+
Така адаптація дозволяє візуально та формально описувати сценарії взаємодії в акторній моделі чату, роблячи її сумісною з традиційними методами формального опису телекомунікаційних систем.
27+
28+
Ключові слова: Message Sequence Chart, Z.120, акторна модель, kernel mappings, чат-система, формальні методи.
29+
\end{abstract}
30+
31+
\section{Вступ}
32+
33+
Сучасні розподілені чат-системи часто будуються на акторній моделі з чітким розділенням між командами (\texttt{Action}), подіями (\texttt{Event}), спостереженнями та предикатами. Репозиторій \texttt{synrc/chat} (проект N2O/SYNRC) містить мінімалістичний \textit{kernel}, де всі поверхневі DSL-команди зводяться до канонічних морфізмів над типами \texttt{Principal}, \texttt{Session}, \texttt{Feed}, \texttt{Message} тощо.
34+
35+
Документ \texttt{ARCH-KERNEL-MAPPINGS.md} явно розмежовує:
36+
\begin{itemize}
37+
\item \textbf{Action} — те, що виконується (Post, Mutate, MarkRead, Replay, View);
38+
\item \textbf{Event} — те, що відбулося;
39+
\item \textbf{Observation} — те, що спостерігається (наприклад, EventObs);
40+
\item \textbf{Predicate} — те, що перевіряється (Seen(...), expect).
41+
\end{itemize}
42+
43+
\textbf{MSC (Z.120)} є ідеальним кандидатом для візуалізації таких мапінгів, оскільки:
44+
\begin{itemize}
45+
\item Фокусується на послідовностях обміну повідомленнями між instances;
46+
\item Підтримує \texttt{alt}, \texttt{par}, \texttt{opt}, \texttt{loop};
47+
\item Дозволяє виражати actions як \texttt{out}/\texttt{in} messages або локальні \texttt{action};
48+
\item \texttt{expect ...} природно відображається через conditions або predicates у розширеннях MSC.
49+
\end{itemize}
50+
51+
Метою роботи є створення формальної відповідності та демонстрація адаптованих сценаріїв у текстовій нотації MSC/PR.
52+
53+
\section{Аналіз мови kernel з synrc/chat}
54+
55+
\subsection{Основні об'єкти (Types)}
56+
\begin{itemize}
57+
\item \texttt{Principal}, \texttt{Session}, \texttt{Feed} (Private, Group), \texttt{Message}
58+
\item \texttt{Event} (Typing, Presence тощо)
59+
\item \texttt{Observation} = EventObs(...)
60+
\item \texttt{Predicate} = Seen(Observation)
61+
\item \texttt{Action} = Post | Mutate | MarkRead | Replay | View | ...
62+
\end{itemize}
63+
64+
\subsection{Ключові морфізми (Actions)}
65+
Канонічні дії:
66+
\begin{itemize}
67+
\item \texttt{Post \{session, actor, feed, payload\}}
68+
\item \texttt{Mutate \{session, actor, target, op\}}
69+
\item \texttt{MarkRead \{session, actor, boundary\}}
70+
\item \texttt{Replay \{session, actor, feed, after\}}
71+
\item \texttt{View \{session, actor, kind, ...\}}
72+
\end{itemize}
73+
74+
\texttt{expect event typing bob1} зводиться не до Action, а до \texttt{Predicate(Seen(EventObs(SessionPresence\{...\}, Typing)))}.
75+
76+
\section{Відповідність між Kernel та MSC (Z.120)}
77+
78+
\begin{table}[h]
79+
\centering
80+
\begin{tabular}{|l|l|}
81+
\hline
82+
\textbf{Елемент Kernel} & \textbf{Конструкція MSC (Z.120)} \\
83+
\hline
84+
Session / Actor / Principal & Instance (lifeline) \\
85+
Post, Mutate, MarkRead, View, Replay & out Message to ... (або action) \\
86+
Event & Message label або inline action \\
87+
Observation (EventObs) & Message з параметрами \\
88+
Predicate Seen(...) / expect & Condition або inline opt/alt з predicate \\
89+
State transition & Message exchange + local action \\
90+
Alternative behaviors & alt ... endalt \\
91+
Parallel events & par ... endpar \\
92+
Sequence of actions & seq (implicit top-to-bottom) \\
93+
Replay after snapshot & loop або MSC reference з after-condition \\
94+
\hline
95+
\end{tabular}
96+
\caption{Відповідність елементів kernel та MSC}
97+
\end{table}
98+
99+
Instances у MSC пропонуються такі:
100+
\begin{itemize}
101+
\item \texttt{AliceSession}, \texttt{BobSession}
102+
\item \texttt{ServerKernel} або \texttt{FeedManager}
103+
\item \texttt{Environment} (для external predicates)
104+
\end{itemize}
105+
106+
\section{Адаптовані приклади в нотації MSC/PR (Z.120)}
107+
108+
\subsection{Приклад 1: Надсилання повідомлення + спостереження typing}
109+
110+
\begin{lstlisting}[language={},basicstyle=\ttfamily\small]
111+
msc SendMessageAndTyping;
112+
instance AliceSession;
113+
out Post {
114+
feed = Private(alice, bob);
115+
payload = {body = "hi"}
116+
} to BobSession;
117+
endinstance;
118+
119+
instance BobSession;
120+
in Post from AliceSession;
121+
action ProcessMessage;
122+
out EventObs(SessionPresence{actor=bob1, kind=Typing}) to AliceSession;
123+
endinstance;
124+
125+
instance AliceSession;
126+
in EventObs from BobSession;
127+
condition Seen(EventObs(Typing));
128+
endinstance;
129+
endmsc;
130+
\end{lstlisting}
131+
132+
\subsection{Приклад 2: Edit message (Mutate)}
133+
134+
\begin{lstlisting}[language={},basicstyle=\ttfamily\small]
135+
msc EditMessageScenario;
136+
instance AliceSession;
137+
out Mutate {
138+
target = ExistingMessage{feed=Private(alice,bob), id="msg-123"};
139+
op = ReplacePayload{body="v2"}
140+
} to ServerKernel;
141+
endinstance;
142+
143+
instance ServerKernel;
144+
in Mutate from AliceSession;
145+
alt
146+
out MutationApplied to AliceSession;
147+
else
148+
out MutationFailed to AliceSession;
149+
endalt;
150+
endinstance;
151+
endmsc;
152+
\end{lstlisting}
153+
154+
\subsection{Приклад 3: Expect + Replay after snapshot}
155+
156+
\begin{lstlisting}[language={},basicstyle=\ttfamily\small]
157+
msc ReplayAfterSnapshot;
158+
instance AliceSession;
159+
out Replay {
160+
feed = Private(alice, bob);
161+
after = Some(AfterFeedSnapshot(id))
162+
} to ServerKernel;
163+
endinstance;
164+
165+
instance ServerKernel;
166+
in Replay from AliceSession;
167+
loop <0, inf>
168+
out Event to AliceSession;
169+
endloop;
170+
endinstance;
171+
172+
instance AliceSession;
173+
condition Satisfies(Predicate(Seen(EventsAfterSnapshot)));
174+
endinstance;
175+
endmsc;
176+
\end{lstlisting}
177+
178+
\section{Переваги адаптації до Z.120}
179+
180+
\begin{itemize}
181+
\item \textbf{Візуальна ясність} — сценарії стають зрозумілими для інженерів без знання OCaml.
182+
\item \textbf{Формальна семантика} — можна використовувати Annex B Z.120 для верифікації.
183+
\item \textbf{Інтеграція з TTCN-3} — сценарії MSC легко перетворюються на тести.
184+
\item \textbf{Масштабування} — High-level MSC (HMSC) дозволяє описувати повний життєвий цикл чату.
185+
\item Сумісність з SDL (Z.100) для повної специфікації стану.
186+
\end{itemize}
187+
188+
\section{Висновки та подальша робота}
189+
190+
Адаптація kernel-мовы з \texttt{synrc/chat} до MSC Z.120 показала високу природність відповідності. Акторні взаємодії, розділення Action/Event/Observation та предикати \texttt{expect} добре відображаються через instances, messages, actions та inline expressions.
191+
192+
Подальша робота може включати:
193+
\begin{itemize}
194+
\item Автоматичну генерацію MSC з kernel-описів.
195+
\item Формальну семантику мапінгу (розширення Annex B).
196+
\item Інтеграцію з інструментами (msc2svg, Telelogic Tau, тощо).
197+
\item Порівняння з UML Sequence Diagrams.
198+
\end{itemize}
199+
200+
\bibliographystyle{plain}
201+
\begin{thebibliography}{9}
202+
\bibitem{itu-z120} ITU-T Recommendation Z.120 (02/2011), Message Sequence Chart (MSC).
203+
\bibitem{synrc} synrc/chat repository, ARCH-KERNEL-MAPPINGS.md, 2025--2026.
204+
\bibitem{annexb} ITU-T Z.120 Annex B (04/1998), Formal semantics of Message Sequence Charts.
205+
\end{thebibliography}
206+
207+
\end{document}

‎priv/msc-z.120.txt‎

Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
Ось детальна BNF-нотація (текстова синтаксична граматика) для Message Sequence Chart (MSC) з ITU-T Z.120.
2+
Зверніть увагу: повна граматика MSC/PR (textual syntax) дуже велика (десятки сторінок у рекомендації Z.120).
3+
4+
Нижче я наводжу основну структуру та ключові production rules з класичної версії (Z.120 1996–2011),
5+
яка використовується в більшості інструментів та літератури.
6+
7+
Meta-notation (як у Z.120)
8+
9+
ITU-T використовує BNF-подібну нотацію з такими правилами:
10+
11+
<non-terminal> — нетермінал
12+
::= — визначається як
13+
— альтернатива
14+
[] — опціонально
15+
{} — повторення 0 або більше разів
16+
() — групування
17+
18+
Термінали пишуться жирним або в лапках (keywords: msc, instance, endmsc тощо)
19+
20+
Основна структура MSC (Top-level)
21+
22+
<msc-document> ::= { <msc> | <hmsc> }*
23+
24+
<msc> ::= msc <msc-name> [ <parameters> ] ;
25+
<msc-body>
26+
endmsc ;
27+
28+
<msc-name> ::= <identifier>
29+
30+
<msc-body> ::= { <instance-definition> | <message-declaration> | <gate-definition> }*
31+
32+
Instance Definition
33+
34+
<instance-definition> ::= instance <instance-name> [ : <type> ] ;
35+
<instance-body>
36+
endinstance ;
37+
38+
<instance-name> ::= <identifier>
39+
40+
<instance-body> ::= { <event> }*
41+
42+
Основні події (Events) на інстансі
43+
44+
<event> ::= <message-send>
45+
| <message-receive>
46+
| <action>
47+
| <timer-event>
48+
| <condition>
49+
| <create>
50+
| <stop>
51+
| <inline-expression>
52+
| <msc-reference>
53+
| <coregion>
54+
55+
<message-send> ::= out <message-name> [ <parameters> ] to <instance-name> ;
56+
57+
<message-receive>::= in <message-name> [ <parameters> ] from <instance-name> ;
58+
59+
<action> ::= action <action-name> [ <parameters> ] ;
60+
61+
<timer-start> ::= starttimer <timer-name> [ <duration> ] ;
62+
63+
<timer-stop> ::= stoptimer <timer-name> ;
64+
65+
<timeout> ::= timeout <timer-name> ;
66+
67+
<condition> ::= condition <condition-name> ;
68+
69+
<create> ::= create <instance-name> ;
70+
71+
<stop> ::= stop ;
72+
73+
Inline Expressions (дуже важливі для сучасного MSC)
74+
75+
<inline-expression> ::= alt <inline-body> endalt
76+
| par <inline-body> endpar
77+
| loop <loop-bound> <inline-body> endloop
78+
| opt <inline-body> endopt
79+
| seq <inline-body> endseq
80+
| exc <inline-body> endexc
81+
82+
<inline-body> ::= { <event> | <inline-expression> }*
83+
84+
High-level MSC (HMSC)
85+
86+
<hmsc> ::= hmsc <hmsc-name> ;
87+
<hmsc-body>
88+
endhmsc ;
89+
90+
<hmsc-body> ::= <hmsc-expression>
91+
92+
<hmsc-expression> ::= <msc-reference>
93+
| <hmsc-expression> ; <hmsc-expression> // seq
94+
| alt <hmsc-expression> , <hmsc-expression> endalt
95+
| loop <loop-bound> <hmsc-expression> endloop
96+
| par <hmsc-expression> , <hmsc-expression> endpar
97+
98+
99+
Приклад простого MSC у текстовій нотації (MSC/PR)
100+
101+
msc ExampleMessageFlow;
102+
instance Alice;
103+
out Hello to Bob;
104+
in Ack from Bob;
105+
endinstance;
106+
107+
instance Bob;
108+
in Hello from Alice;
109+
action ProcessMessage;
110+
out Ack to Alice;
111+
endinstance;
112+
endmsc;
113+
114+
Більш складний приклад з inline expression
115+
116+
msc LoginScenario;
117+
instance User : Client;
118+
out LoginRequest to Server;
119+
endinstance;
120+
121+
instance Server;
122+
in LoginRequest from User;
123+
alt
124+
out LoginOK to User;
125+
else
126+
out LoginFailed to User;
127+
endalt;
128+
endinstance;
129+
endmsc;
130+

0 commit comments

Comments
 (0)