Дополню, раз уж тут такая пьянка завелась. В смежной теме была хорошая статейка насчёт проблематики проверок в целом:
Specification and Validation of Embedded Systems: A Case Study of a Fault-Tolerant Data Acquisition System with Lustre Programming environment, где подчёркивается такое свойство верификации как “locally” в отношение всей системы:
Цитата:
Ideally, the formal verification of such a program should
consist of comparing it with a global, abstract specification.
As it is often the case with real case-studies, this specification
is not available. The problem even more serious, here, since
the abstract specification of such a fault-tolerant system
should probably involve probabilistic properties, which are
stated nowhere, and which could not be handled by usual
verification tools.
So, we don’t know “what to verify” on the complete
program. However, there are two common cases where
verification tools can be applied “locally”:
* When there are two ways of writing a node, one can write
both and try to show that they are equivalent. If they are
not, a bug is detected, at least, in one of them. If they
are, this increases the confidence one can have in any of
them. We will illustrate this situation on two versions
of the node "values_nok", which detects cross-channel
faults.
* When some consistency properties are clearly expressed
in the requirements: for instance, we will try to prove
that at most two channels can become “reset-inhibited”
Т.е. базовый язык как Lustre даёт гарантии завершимости, но как только начинаются "танцы с бубнами" по конкретной предметке -- неизбежно лишь частично по потребности (и обычно после первичного тестирования) начинаются всякие верификации отдельными кусками (причём “locally” не зависит от инструментов или языков -- общий результат сути верификации как таковой в целом).
Однако фишка "синхронной школы" в этом:
Илья Ермаков писал(а):
Собственно, мы тут уже обсуждали, что всё идёт к тому, что в центре разработки - системная модель (при этом единая для разработчиков СУ и для системных инженеров),
а от неё уже идёт проектирование СУ и порождение кода (автоматическое или частично автоматическое).
...
Вообще, технологии, основанные на выделении состояний - это хорошо.
Но с примитивными КА не всё гладко. Как только начинаешь разделять состояния МОДЕЛИ управляемой системы и внутренние состояния самой управляющей системы...
Т.е. вопрос развития этих подходов стоит.
Вы же приводите как раз уже нечто другое, чем Эстерелевские диаграммы состояний.
Полноценные языки программирования.
Так вот, здесь именно что "язык программирования" и "модель системы" -- в одном флаконе. Была попытка уточнить принцип взаимодействия автоматов:
viewtopic.php?f=152&t=6049#p101208, но сложно кратко описать суть. Попробую чуть подробней.
Итак, ранее в той теме были ссылки, к примеру, на провал "состояний типов" в Rust-e:
http://pcwalton.github.io/blog/2012/12/ ... e-is-dead/А собирались там реализовать технику как в Vault -- экспериментальное расширение С от MS:
https://www.microsoft.com/en-us/researc ... pldi01.pdfВ данном случае подразумевается поддержка "протокола ресурсов" -- отслеживание порядка операций над объектом (а также "время жизни" -- регионы памяти), представляя последний как виртуальный автомат -- см. рисунок:
Вложение:
protocol.png [ 51.55 КБ | Просмотров: 7325 ]
В общем случае требуются двусторонние и более протоколы взаимодействия. В программистской интерпретации -- "сессионные типы":
http://simonjf.com/2016/05/28/session-t ... tions.htmlТема тяжёлая. Однако, "французы" в 80-х не страдали отдельными языками разработки для указания взаимодействия, как, напр., Scribble (выше по ссылке). Всё в рамках "обычного" -- пишется код работы процессов, проверяется и т.д. Затем по потребности при генерации кода на С или спецификаций для железа процессы могут быть "разрезаны" -- разнесены по узлам, программам и т.д., в т.ч. формируется подсистема сетевого взаимодействия и т.п. по потребности.
Вот в этой статейке про "объекты-автоматы":
https://pdfs.semanticscholar.org/f570/9 ... 83acca.pdfнаглядный пример автоматического определения протокола на основе кода программ (спецификации, конечно, могут быть указаны и вручную).
Подобную технику возможно обобщить через систему типизации, с учётом "разрыва" типа. Можно воспользоваться примером реализации сессионных типов для Java:
Type-Safe Eventful Sessions in Java, где на борту имеются механизмы runtime-нарезки сессий -- т.е. "разрыва" типа-сессии (см. оператор typecase и пр.). В данном случае пример реализации вэб-сервера, где ядро программы как подсистема ввода/вывода вокруг сокетов, обслуживающее много клиентов. При возникновении событий (коннекты, получение данных) -- виртуально "воссоединяются" серверный и клиентские процессы -- возобновляется обработка данных по протоколу.
По таким мотивам. Определим некий протокол взаимодействия, псевдокод:
Код:
procedure Protocol(A, B: side) = (s: string);
{
START:> var i at A: int = proc1();
ST1:> var f at B: float = proc2(i);
ST2:> s at A = proc3(f);
}
Пусть это будет некая реальная программка, проверяемая по ранее указанным техникам. Здесь "side" -- специальный тип, символизирующий сторону контракта -- как, напр., в том же Scribble. Про оператор "at" здесь подробнее:
http://www.di.ens.fr/~guatto/papers/lctes12.pdf, т.е. это указание "региона" как в Rust (но техника в целом значительно проще), однако в данном случае понимается по-особому (виртуально) из-за использования типа side. Запись вида "START:>" -- обычные label в ML-стиле (главное идентифицировать процессы, в принципе достаточно переменных-"сигналов"). Код понимается примерно так: выполняется proc1 условно на стороне A, затем proc2 (использующий результат от poc1) на стороне B и т.д.
Теперь можем определить некий процесс "воссоединения", пусть на стороне вэб-сервера -- сторона А, т.е. где-то на сервере при сокет-событиях будет выполняться "продолжение" сессии:
Код:
procedure SomeProc(h: handle, o: object; var ts: typestate[h, Protocol(_,*)]);
{
match ts with
| START =>
var i: int = o.get_data;
write(h, i);
| ST1 =>
var f = read[float](h);
ST2(f);
| ST2(f: float) =>
o.set_data(f);
end;
}
Здесь аргументы: "h: handle" -- дескриптор для ввода/вывода (некий сокет), "o: object" -- какой-то объект на сервере, исполняющий "o.get_data" -- это есть proc1 по протоколу, "o.set_data" -- proc3.
Аргумент "var ts: typestate[h, Protocol(_,*)]" -- специального типа для отслеживания состояния сессии, параметризуется каналом связи и протоколом (символы "_" и "*" -- согласно обычному pattern matching -- некое значение и его отсутствие соответственно -- так указали, что задействована сторона A). Для аргумента ts компилятор отслеживает операции -- переходы на условные состояния сессии, и корректирует его значение -- подробнее см. "Sessions in Java" выше.
Предполагается, что компилятор понимает семантику операций вида read, write, flush и т.п. для ввода/вывода, соответственно и контролирует порядок их применения. Полагаю, смысл кода очевиден без уточнения. Оператор match в данном случае напоминает "автоматы", как здесь (про "automaton" или "mode"):
viewtopic.php?f=152&t=6049#p101207В примере, прежде всего, контролируется семантика сетевого взаимодействия или ввода/вывода. Контроль операций для "o: object" -- "get_data/set_data" -- через свой протокол типа. Или же расширить typestate выше.
Переменные типа typestate -- неизбежны в любом случае, как бы вручную не реализовывались бы "сессии". Однако этот флаг пусть лучше контролирует компилятор.
Такая техника универсальна. К примеру, если определить кортеж вида (h: handle; ts: typestate), то компилятор всегда сможет отслеживать корректность, даже если переменные "улетают" из области видимости, к примеру, вносятся/извлекаются в контейнеры данных.
В общем, примерна такова политика для языка программирования. Причём годится она для реализации как и для жёсткого realtime, так и для попсового текстового редактора. Проверки по потребности, где-то рядом сбоку, с учётом "разрыва" типа.
В целом задачи верификации, конечно же, шире. Здесь на форуме когда-то был представлен ГрафКонт -- специфичные отношения между процессами. Возможно допустимо понимать их как дополнительные ограничения в протоколах, в т.ч. и для синтеза систем (или решения задач планировщика).
Вот ещё пример отношений между процессами (с картинками):
Contracts and Behavioral Patterns for SoS: The EU IP DANSE approachИли же подобные отношения выражаются через "сигналы" у тех же "французов" (для периодических процессов с разными частотами):
A Real-Time Architecture Design Language for Multi-Rate Embedded Control Systems