OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Среда, 13 Декабрь, 2017 13:48

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 34 ]  На страницу Пред.  1, 2
Автор Сообщение
СообщениеДобавлено: Пятница, 07 Июль, 2017 21:05 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 189
В принципе, и вокруг мейнстрима были и есть здравые идеи. Напр., во времена моды "аспектно-ориентированности" была такая академическая задумка:
http://ptolemy.cs.iastate.edu/papers/ECOOP.08.paper.pdf

где видна попытка уменьшить "callback hell" в типовой объектной модели. Также там неплохо обобщены основные проблемы "аспектности".
Это всё к той же отмеченной ранее проблеме координации "верхнего уровня".

Для языка аля Lucid Synchrone достаточно паттерна "декоратор", т.е. переопределения функции. К примеру, для какого-то scope можно ввести модуль с альтернативной реализацией:
Код:
fn my_func(s: string) => print s;
...
// переопределяем ф-цию
impl fn my_func(s: string) =>
{
  inherit(s);  // вызов исходной ф-ции
  print 'ok';
}


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 09 Октябрь, 2017 20:18 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 189
viewtopic.php?f=31&t=6128#p102165
prospero78 писал(а):
И всё-таки верификация не решает проблем системы и сети. Это ооочень накладно. Где-то видел шуточный селфтест: он проверял правильность того, что процедура принимала два числа и всегда возвращала ноль. Исполнение -- идеальное. Смысл? Верификация верифицировала процедуру на то, что та работает верно, результат смысла не имеет.
Опять же, как верифицировать результат при квантовых вычислениях? Это точно возможно?
Считаю подход Вирта -- строить программы в оборонительном стиле -- достаточным вместе с контрактным программированием.
Многопоточность и многопроцессность -- особенно последнее -- требует усилий. Что-то, конечно можно сделать. Даже наверное нужно (раз Дмитрий сделал).
Но важно вовремя остановиться. Чем изощрённей методика -- тем больше вероятность ошибки. А нет ничего дороже на этом свете чем глупость.

Так ведь верификация и есть "контракты" для "оборонительного стиля". Фактически, единственное существенное отличие от традиционных "assert"-ов в runtime (во время интерпретации модели) -- попытка анализа в compiletime или на этапе построения модели.
Если написали "контракт" в виде требования возвращать ноль при любом входе -- значит, такова цель, и осмысленность возникает соответствующая такой цели. А формально выделяют задачи верификации (лат. verus -- верный) -- соответствие установленным требованиям, и валидации (validus -- здравый) -- соответствие самих требований целям системы.
Если единый "assert" покрывает всю систему -- повезло. Но обычно картина локальная -- здесь конкретная цитата по поводу:
viewtopic.php?f=152&t=6126#p102121

И, как правило, "assert" зависит от конкретики алгоритма, и на конкретику влияет "репертуар" исполнителя -- его используемые команды, свойства и т.п. -- в этом лишь разница в понимании того, кто там пашет в реалиях -- человек, биомолекула или квантовый исполнитель.

Детальнее о проблемах сети (и в целом о проверках). Пусть у нас возникает потребность реализации процессов в виде какой-то транзакции (пусть даже финансовой) аля "A(K) -> Б(C) -> В(K) -> Г(C) ...", т.е. последовательность (грубо) процессов "A, Б ...", каждый из которых исполняется либо на "сервере" (С) или на "клиенте" (K). В общем, распределённые процессы (в целом на множестве сторон взаимодействия) осуществляют виртуальные транзакции, определяемые протоколом, условно постоянно появляющиеся в системе. В любой программе, каким-то способом реализующей процесс транзакции, как правило, можем выделить подсистему ввода/вывода -- условно доставку данных, и прикладную предметную реализацию транзакции Эти две подсистемы имеют точки соприкосновения.
Полагаю, не ошибусь, если предположу следующий типовой сценарий, характерный в большинстве случаев. Обычно в сетевом вводе/выводе задействованы таймауты, при истечении которых незавершенные операции считаются неудачными -- предполагается ненадёжная среда доставки, и выполняется повторное выполнение (с возможным частичным восстановлением каких-то данных) транзакции по потребности, или же прочие необходимые реакции. Однако в каких-то случаях сигналы (данные) могут отсутствовать при причине deadlock-ов и/или livelock-ов (кто-то где-то заблокирован в ожидании результатов друг друга, прямо или косвенно, или же кто-то условно "зациклился", или же технически заблокирован тред ОС, назначенный для исполнения некоторых процессов, и т.п.). В каких-то системах подобные ситуации допускаются априори (ибо заранее невозможно установить правильную модель вычислений -- нет протокола, как такового), или же "глюки" возникают из-за неправильной логики протоколов взаимодействия. В последних случаях глюки могут быть разрулены также, как и глюки среды доставки данных (таймауты), но не всегда -- в тех случаях, когда глюки протоколов возникают относительно редко, при повторном исполнении транзакций возникает иная предыстория вычислений, и в итоге всё "ок". В иных случаях проблема со временем может оказаться локализованной -- "ой, извиняемся, быстро исправляем ...". А где-то обстоятельства нагибают более ответственно. К тому же в общем случае возможно хоть и распределенное взаимодействие, но в рамках условно надёжной шины обмена данными.

В статейке ниже наглядный пример выявления глюков в протоколах взаимодействия, в данном случае -- академическая работа над контрактами каналов в Singularity ОС -- был когда-то эксперимент от MS в ответ на возникшую тогда моду на "акторы":
Вложение:
Analyzing Singularity Channel Contracts.pdf [235.81 КБ]
Скачиваний: 7


Причём проблемки выявлены после заявлений разработчиков, мол всё норм (хотя эксплуатации ОС не было, как таковой). И масштабы взаимодействующих автоматов (контрактов) малые -- вполне обозримы графы переходов, но визуально глюки незаметны (ну или необходимо сильно напрягаться для мысленной интерпретации исполнения).

Это пример "неглупости" проверок. В данном случае используется иной инструмент, не "Net-платформа" и "C#" -- нет возможности написать какие-то "runtime assert"-ы в таком языке как C# в подобных случаях (конкретнее -- проверка через Spin (инструмент) с генерацией моделей для Promela (язык "программирования"), а исходные контракты в Singularity определяются на своём DSL).
Здесь первый подход -- проверка формальных моделей взаимодействия. Методики и инструменты разные, но общий принцип -- найти пример (или контрпример) нарушения требований. Более широко -- проверить достижимость (отсутствие deadlock-ов), "справедливость" (отсутствие livelock-ов), безопасность -- конкретные предметные "assert"-ы. Для упрощения можем обобщить как задачи принципиальной достижимости и безопасности. И очень грубо говоря, делается попытка представить взаимодействие процессов в виде последовательного протокола по мотивам выше, с учётом зависимости по данным, параллельной (со своим исполнителем) работы, с учётом возникающих в итоге возможных вариантов "совместности". О последнем явлении здесь на форуме была когда-то ссылка на статейку Эдвард А. Ли, где представлена простейшая матем. интерпретация:
https://habrahabr.ru/company/nordavind/blog/195262/

Но ключевое в подходе выше -- проверяется модель вычислений или протокола, а сама реализация конкретных процессов -- отдельная песня, соответствие реализации исходной формальной модели -- отдельные задачи.

В платформах вокруг Esterel такие языки как Lustre/Signal/Lucid Synchrone -- пример языка моделирования и реализации в "одном флаконе". Любая программка (каждая функция, или "node/task") по конструкции имеет гарантию принципиальной достижимости. Здесь компилятор анализирует возможность возникновения/отсутствия данных (сигналы), выявляет зависимости по данным и возможность взаимозависимости (deadlock-и, а также по возможности и livelock-и), проверяет правильность веток "if" -- все ли указаны варианты, нет ли "if" без "else" или определена ли реакция на отсутствие вычисления (данных), и т.д. и т.п. Высказывание упрощённое, поскольку расширенно в потоковых моделях вместо (или в дополнение) "if" имеются специализированные операторы "фильтра" данных (или undersampling, а также oversampling), алгебраические типы и пр. Т.е. имеется базовый анализ семантики языка, ну и далее по потребности и возможности -- вплоть до дедуктивных систем проверок ("зависимых типов", и основополагающие понятия "сигналов" -- всё через типы). Есть спец-библиотеки для построения и систем эмуляции с недетерминированным выбором данных/вычислений -- для тестирования, грубых прикидок и т.д. Причём принцип реализации -- поближе к "Бёма — Якопини" (базовые структуры процессов) да предметные уточняющие "assert"-ы для "безопасности", а необходимые "теоремы" да "леммы" -- автоматом за кадром. И, конечно же, "hard-математика" на борту для случаев необходимости.
Ограничения платформы позволяют относительно эффективно использовать инструменты. В случае динамики изменения структуры процесса/процессов -- возникают сложности, теоретически покоряемые, но гораздо труднее (в целом, для любой возможной платформы):
viewtopic.php?f=152&t=6126#p102120

Итак, реализовали программку -- получили проверенную "синхронную" модель протокола работы процессов. Теперь есть возможность контролируемо сгенерить локальную или любую распределенную реализацию процессов.

Насчёт локальной модели реализации. Потоковая модель предполагает ярусно-параллельную форму асинхронности, или расширенно как на рис.:
Вложение:
async_dataflow.png
async_dataflow.png [ 19.5 КБ | Просмотров: 265 ]

Пример техники построения -- ниже (здесь уже была ссылка), причём форма консервативна в том смысле, что при отсутствии реальных альтернативных исполнителей модель остаётся синхронной -- т.е. первично можно моделировать процессы синхронно, затем по необходимости развивать "ускорение":
Programming Parallelism with Futures in Lustre

Можно обратить внимание на применение "буферов" или "задержек" -- приятнее, когда их правильность контролирует компилятор. Как и прочие атрибуты (напр., приоритеты процессов), или "перегрузку/недогрузку" и достижимость в этом контексте:
Transaction Parameterized Dataflow: A Model for Context-Dependent Streaming Applications

Насчёт распределенности. Зная модель вычислений (исходный протокол взаимодействия) и принципы конкретной подсистемы ввода/вывода или среды доставки данных -- очевидно, возможен требуемый синтез системы. В общем случае под средой доставки можно понимать всё, что угодно. К примеру, наличие подсистемы publish-subscribe (процессы могут работать в разном временном разрезе), использование GUI-интерфейса и взаимодействие с пользователем, и т.п.
На форуме Дракон-а когда-то была ссылка на проект Termite -- "интеллектуальный" синтез программ реализации драйверов:
http://ssrg.nicta.com.au/projects/TS/drivers/synthesis/

, где автоматический синтез на базе теории игр как поиск оптимальной траектории системы (т.е. синтезируется даже исходный протокол по предопределенным правилам "игры"). Любопытный обзор инструментов для этого:
https://arxiv.org/abs/1506.08726

Проект выше демонстрирует важную особенность -- в общем случае возникает необходимость частичного, постепенного, инкрементального построения конечной системы, в том числе и вручную. Для этого неизбежно необходимо понимать "протоколы". Здесь уточнения:
viewtopic.php?f=152&t=6126#p102121

, где акцентируется на "разрыве" протокола или его интерпретацию в рамках типов -- "сессионные типы", "состояние типов", "протоколы ресурсов". Там же есть пример (по ссылке в сообщении) реализации вэб-сервера -- демонстрации "разрыва" предметного протокола, ну и сетевого взаимодействия. В целом, очевидно, что в системе возникает множество "протоколов" -- свои для реализации "прикладных транзакций" и сопутствующие "технологические" -- другие подсистемы доставки данных или какие-то смежные (все подсистемы проверяются по своим протоколам, в т.ч. возможен протокол их состыковки).
Ключевое, если возникает потребность контролирования реализации со стороны компилятора, и как бы не взаимодействовали подсистемы -- неизбежно на практике требуется "разрывать" тип или "assert". По ссылке выше был пример, он, конечно же, так себе... Для раскрытия темы -- необходима детальная содержательная постановка (вне рамках данного сообщения форума).

Итого, если в базовом языке или платформе на борту будут необходимые инструменты -- "верификацией" придётся заниматься, может быть, даже незаметно (отчасти).


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 09 Октябрь, 2017 20:22 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 189
Насчёт протоколов сетевого взаимодействия. В статейке ниже полезная академическая разработка, но принципы применимы широко:
A Prescription for Safely Relaxing Synchrony

Здесь техника организации "спекулятивных вычислений" для ускорения -- автоматом на основе понимания исходного синхронного протокола взаимодействия процессов (в данном случае -- в рамках ML-программ с использованием примитивов библиотеки ConcurrentML) выдвигается предположение соблюдения последовательности выполнения процессов в распределенной среде -- если где-то некий А начал свою работу согласно протоколу ранее прочих узлов в сети, то и его результаты будут доступны ранее других, а также определяется допустимость независимого или совместного исполнения процессов. Если в сети нарушается последовательность получения результатов -- анализируется возможность и организуется кэширование данных, в противном случае осуществляется перезапуск транзакции, но уже с политикой явного ожидания данных (блокировка).
В общем, демонстрация облегчения ручного ломания головы. А также хороший контекст в том, что целенаправленная распределенность часто влияет на структуру алгоритма "протокола". Возможное "ускорение" того же исходного протокола, напр., для локальных асинхронных dataflow-процессов, скорее всего, будет построено по-иному, со своими техниками оптимизации, и под конкретное железо или набор исполнителей.

В целом, конечно, протоколы зависят от специфики задач. К примеру, в проекте Bloom:
http://bloom-lang.net/index.html

анализируется "монотонность" вычислений -- взаимодействующие процессы понимаются как виртуальные (или реальные) БД, и осуществляется контроль недопустимости операций, нарушающий контекст предыстории вычислений в заданных аспектах (кроме "попсового" Ruby-like имеется и диалект Datalog-а (или Prolog-а) для разработки и верификации -- там это "низкий" уровень).


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 10 Октябрь, 2017 11:58 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 1049
Откуда: СССР v2.0 rc 1
Не сомневаюсь, что на уровне протокола можно защитить данные от принципиально потенциально кривого канала связи.
Если бы это было не так, речь была бы невозможно. Верификация тут не нужна, валидация осуществляется формально. И если с последней особо вопросов нет, то верификация поверх даже статических систем возможна лишь частично. Есть достаточное число алгоритмов, которое и статически верифицировать не возможно. А ведь есть ещё динамика...
Собственно, не так интересно внутреннее состояние системы, как всё те же пришлые варяги во время работы. В каком-то смысле вирусы -- незаконно верифицированные программные модули. И ровно половина из них убивается на корню просто запретом использования адресной арифметики, как источником сбоя стека.
Это просто ограничения языка, которые, по хорошему -- следовало бы вынести на уровень железа. Но это так, цветочки. Сколько ещё можно упростить неликвидного поведения программной системы рамками языка?
И кстати, на много упрощается валидация (в идеале, её даже можно исключить в силу "бесплатной" валидации исходного текста). И также существенно упрощается верификация. Как побочный эффект. Это будет даже не 80, а под 95% искомого эффекта без дополнительных усилий. Оставшиеся 5%, имхо, на текущем уровне (массовом) развития ИТ -- пока будут неэффективными тратами ресурсов. Тут хотя бы эти 95% реализовать ,а там, глядишь, и новые методы замаячат. Более простые и не менее эффективные. (* Прям по Гегелю получается ))) *)


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 10 Октябрь, 2017 19:16 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 189
prospero78 писал(а):
Сколько ещё можно упростить неликвидного поведения программной системы рамками языка?
И кстати, на много упрощается валидация (в идеале, её даже можно исключить в силу "бесплатной" валидации исходного текста). И также существенно упрощается верификация. Как побочный эффект.

Кстати, термины валидация и верификация, всё-таки, резиновые. Иногда подразумевают контекст "жизненного цикла": верификация -- подготовка для "сдачи в эксплуатацию" (со всеми проверками), валидация -- "приёмка заказчиком", мол опять проверки, насколько система отвечает "ожиданиям".
В программной интерпретации, видимо, следует понимать так. Воспользуюсь неоднократно упомянутым проектом F-star (как один из самых продвинутых инструментов дедуктивной верификации, под крышей MS), конкретнее -- пример просто для наглядности:
Probabilistic Relational Verification for Cryptographic Implementations

и на основе спецоператоров (согласно статейке выше) L() и R() -- "левый" и "правый" вызов функции -- для указания отношений между смежными тактами автомата -- выразим условие монотонности для функционального типа:
x: int -> y: int {L(x) <= R(x) ==> L(y) <= R(y)}

Это пример того, что подобные условия на runtime-assert-ах не укажешь -- функция ведь не содержит состояния, runtime-assert-ы возможны лишь для имитационного моделирования -- в контексте иной функции в рамках тестирования, т.е. для "эмулятора".
Возможные функции с таким типом вставляются в код, как строительные кирпичики. Валидация -- проверка состыковки ограничений типа во всех кирпичиках (т.е. проверка "сводимости" типов). Верификация -- проверка соответствия конкретных реализаций функций своим типам.

Ограничения типов, кстати, можно прикрутить не только к верификации, но и для задач документации, тестирования (генерация тестов), синтез реализаций и т.п.

В том же проекте F-Star, к слову, есть интересные (это мягко сказать) техники верификации, в том числе для выявления "незаконно верифицированных" -- для задач крипто-безопасности, к примеру (здесь опять же построение принципиального устройства протокола, технология отлична от того же упомянутого SPIN и ему подобных):
Wys*: A Verified Language Extension for Secure Multi-party Computations


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 08 Декабрь, 2017 20:56 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 189
viewtopic.php?f=152&t=6158&start=40#p102994
Дмитрий Дагаев писал(а):
Вот еще интересная цитата из AREAVE OASIS касательно Esterel и Lustre:
Цитата:
Synchronous languages like Esterel [4] or Lustre [5] relies on strong formal definitions, and allows for formal checksand validations of the modeled system. This permitted their use in critical environments and especially for aviation and transportation. Nonetheless, for the concrete implementation of a synchronous model, the usual approach is either to generate C code for a Posix compliant RT kernel (e.g.VxWorks) or generate statically scheduled sequential C code for a barebone execution (or on top of interrupt services,e.g. [ссылка 6]). The former is nearly impossible to validate with regards to the standards. The later could probably be away to generate an application in the traditional design of ISO-60880 (periodic execution of a single program divided as statically scheduled RT activities). Nonetheless, to our knowledge, no efforts were made toward such a goal. Webelieve that aiming to such a goal would be achievable but would not reduce the cost of validation, even thought the cost of programming would be roughly on par with OASIS.

Злыми конкурентами утверждается, что синхронные языки не подходят под 60880 из-за реализации. Ничего такого не сделано. При этом второй вариант, кажущийся приемлемым, на самом деле оставляет много вопросов, например в части кучи GOTO, необходимости специальных компиляторов для Lustre с измененной семантикой.

На сайте Esterel заявлена совместимость в т.ч. и с 60880 для их SCADE, но за подробностями отправляют в службу продаж:
http://www.esterel-technologies.com/ind ... tification

Однако, в целом, любопытно (и полезно) оценить возможности используемого языка, точнее понять его ограничения (на фоне мэйнстрима). Всё-таки, не только академический проект, но и широкая промышленная эксплуатация.
Ниже краткий обзор диалекта Lustre, применяемый в SCADE (причём в текстовой форме, раскрывая содержательный смысл того, чего там зарисовывают в диаграммах):
Scade 6: A Formal Language for Embedded Critical Software Development

Базовые принципы кодогенерации:
Clock-directed Modular Code Generation for Synchronous Data-flow Languages

Сам императивный язык Esterel был "закрыт" в 2008 г. на версии V7, тюненгованный для hardware-реализации, но проблематичный для эффективной software-реализации, в т.ч. была затруднительна статическая верификация (согласно док-м). "Императивщину" в Lustre добавили конструкциями "activate if ..." для блоков уравнений, "automaton", измененной поддержкой массивов.

Явные "автоматы" соответствуют понятию "высокоуровневых гиперпроцессов", плюс явная иерархическая и параллельная композиция функций-состояний:
http://forum.drakon.su/viewtopic.php?f= ... 64#p100964

На фоне ограничений даже не заметны на первый взгляд такие фишки, как примитивный полиморфизм (выше по ссылке есть примеры декларации процессов с абстрактным типом numeric и применении процессов с конкретным float).


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 08 Декабрь, 2017 21:00 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 189
viewtopic.php?f=86&t=6188#p103053
Comdiv писал(а):
Исходя из рекомендаций к коду для атомных станций, которые регламентируют, что цикл должен иметь константное максимальное количество итераций и того, что в общем случае проанализировать количество итераций для инструментальных средств может быть затруднительным, то, по-хорошему, язык должен предоставлять цикл подобного вида:
Код:
Loop =
  IdentOk ":=" LOOP Limit WHILE Expression DO
    Statements
  END .

Limit = ConstExpr | MIN(ExprLimit, ConstExpr) .

Или какого другого? Или не должен?

В SCADE нет явных циклов. Предоставляются средства для работы с массивами. Поначалу были "slices" (удобные для hardware-реализации), но затем их заменили "итераторами"-функциями:
http://laure.gonnord.org/pro/research/E ... arrays.pdf
https://link.springer.com/content/pdf/1 ... F59130.pdf

Базовые итераторы -- типовые для "функциональщины": map, reduce, fill, map_reduce, forall. С возможностью оптимизаций ("склейки" операций и избегания лишних циклов и построения промежуточных структур). Прочий функционал подключается как "external".

Примечательно, что доступ к элементу массива по индексу запрещён на основе динамических выражений, т.е. допустим доступ только на основе константных выражений, определяемых ещё в compiletime. Даже нет проверок в runtime насчёт корректности диапазонов для массивов.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Пятница, 08 Декабрь, 2017 21:32 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 197
Откуда: Москва
PSV100 писал(а):
На сайте Esterel заявлена совместимость в т.ч. и с 60880 для их SCADE, но за подробностями отправляют в службу продаж:
http://www.esterel-technologies.com/ind ... tification
..
В SCADE нет явных циклов.

Если Вы заметили, я упоминал средства здесь, но разумно предоставил слово разработчикам AREVA - их прямым конкурентам.

Можно внимательно ознакомиться с представленной ими Certification Kit и непосредственно сертификатом.
Представленный сертификат:
1. По стандарту 61508, т.е. может быть и 60880, и 62138 - а это уже категории B, C;
2. Сертификат выдан на кодогенератор на обычной ОС, а не на рантайм, где реальное время, циклы и все жесткие требования. Я это упоминал.

Так что, когда столь серьезная компания получит сертификаты, она их обязательно опубликует. А пока ...
Если у Вас будет информация, давайте ссылки, очень полезно!


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 11 Декабрь, 2017 20:17 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 189
Дмитрий Дагаев писал(а):
Если Вы заметили, я упоминал средства здесь, но разумно предоставил слово разработчикам AREVA - их прямым конкурентам.

Ранее читал Ваши сообщения, но они подзабылись. Когда наткнулся на публикацию по поводу языка SCADE (выше представленную), вспомнилось лишь процитированное мной Ваше замечание, соответственно без прочих деталей.
Дмитрий Дагаев писал(а):
Сертификат выдан на кодогенератор на обычной ОС, а не на рантайм, где реальное время, циклы и все жесткие требования...

Насколько я понял, сертифицированные тулзы должны запускаться на определенных версиях винды, т.е. есть требования к исполнительной среде для самого компилятора и остальных инструментов. А вот конкретика целевых платформ, для которых генерируется код и прочее, не раскрыта.

В общем-то, я лишь акцентирую на языковом аспекте, на соответствие модели вычислений жёстким стандартам (но в стандартах и сертификации я не очень-то спец, впрочем как и в области embedded).
Дмитрий Дагаев писал(а):
Если у Вас будет информация, давайте ссылки, очень полезно!

Про SCADE в целом очень мало общедоступной информации про технические детали, на любой чих отсылают в службу продажи. В своих разборках с dataflow-языками я лишь косвенно наблюдал материалы про runtime-платформы или модели исполнения. Здесь в теме были некоторые ссылки. Повторю (с дополнениями), вдруг что-то найдётся полезное. Но ничего не могу уточнить насчёт соответствия каким-то стандартам. Полагаю, при потребности возможен уже более предметный разбор полётов.

"Квази-синхронные" процессы -- совместно работающие (асинхронные) процессы, взаимодействующие через общую память по некоторым правилам (методика была первично обкатана на Airbus-ах):
https://www.lri.fr/~mandel/papiers/Halb ... D-2006.pdf
https://tel.archives-ouvertes.fr/tel-01545630/document

(по первой ссылке -- кратко, по второй -- развёрнуто, с использованием языка Zélus -- подготовка внедрения в SCADE гибридных (дискретно-непрерывная семантика) автоматов).


На глаза попадался Prelude -- язык описания архитектуры в стиле Lustre-like с realtime-ограничениями. Но это уже не Esterel и не SCADE. Краткое введение и диссертация с подробностями:
http://www.cristal.univ-lille.fr/~forge ... -SAC10.pdf
http://www.cristal.univ-lille.fr/~forge ... thesis.pdf

Вокруг него были всякие публикации насчёт платформ, к примеру -- под многоядерные (многопоточные) архитектуры:
http://www2.compute.dtu.dk/~wopu/papers/fmtv14.pdf


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 11 Декабрь, 2017 20:23 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 189
PSV100 писал(а):
В SCADE нет явных циклов. Предоставляются средства для работы с массивами. Поначалу были "slices" (удобные для hardware-реализации), но затем их заменили "итераторами"-функциями...

Да, и функционал циклов также реализуется через явные "автоматы" -- конструкция "automaton". К тому же, в целом, тамошние "node" -- сами по себе есть реагирующие автоматы с "вечным" (циклическим) исполнением.

Однако, семантика Lustre подразумевает, что "главная" node (аля "main"-функция в программе, содержащая вызовы прочих суб-node) исполняется после получения всех необходимых входных данных. Т.е. при генерации конечного исполняемого кода (или спецификации для "железа") исходный код для node заворачивается в операции ввода/вывода (и прочего необходимого) согласно требуемой платформе ("главных" node может быть множество). Семантика же императивного языка Esterel заключается в "мгновенной" реакции на возникновение сигнала: при операциях аля "emit" -- "широковещательной" эмиссии данных (сигналов) -- условно сразу же реагируют параллельные процессы (сопрограммы) на ожидающих операциях вида await.
Пример поддержки "мгновенно реагирующей" семантики в самом языке Lustre здесь уже был -- проект InteLus (вроде пока академический, но под крышей Esterel) -- расширение Lustre для дополнительной управляющей логики:
Sheep in wolf’s clothing: Implementation models for data-fl̘ow multi-threaded software

Здесь, прежде всего, многопоточное управление. Базовая модель исчисления "clock"-ов расширяется мат. моделями согласованности операций с памятью, семафорами и пр.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 11 Декабрь, 2017 20:26 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 189
PSV100 писал(а):
Сам императивный язык Esterel был "закрыт" в 2008 г. на версии V7, тюненгованный для hardware-реализации, но проблематичный для эффективной software-реализации, в т.ч. была затруднительна статическая верификация (согласно док-м).

Есть такой язык Quartz -- императивный в стиле Esterel:
http://www.averest.org/

с некоторыми фишками "классики" data-flow (напр., поддержка default-значений для переменных -- символизируют состояние "проводов" в цифровых схемах, когда как прочие "переменные в памяти" -- аля "регистры". Вместо типовых операций вида "pre" -- сохраненные результаты вычислений на предшествующем такте -- используется оператор "next", видимо из-за используемых верификаторов семейства SMV, как NuSMV).

Однако, чтобы программы были "корректными по конструкции", вынужденны были добавить исчисление "clock"-ов, в данном случае на базе языка Signal. Ниже подробнее (где, прежде всего, раскрыта мат. семантика языка Signal в виде операционной интерпретации):
Constructive polychronous systems


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 11 Декабрь, 2017 20:33 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 189
Интересна платформа Heptagon (вроде как, здесь также видны следы Esterel по некоторым именам авторов публикаций, всё open source):
http://heptagon.gforge.inria.fr/

Ранее были уже ссылки насчёт расширенной поддержки массивов (с оптимизацией):
http://www.di.ens.fr/~guatto/papers/lctes12.pdf
и реализации асинхронных data-flow процессов:
https://www.di.ens.fr/~pouzet/bib/emsoft12.pdf

Но основное -- поддержка "discrete controller synthesis" -- синтез программ управляющей логики на основе ограничений (язык Lustre расширяется специальными контрактами). Кратко:
Contracts for modular discrete controller synthesis

Один из вариантов прикладного применения -- поддержка т.н. самоадаптируемых систем -- динамическое изменение конфигураций систем в зависимости от условий окружения. Вместо ручной алгоритмизации выполняется анализ возможности построить систему, и, собственно, генерируется решение (что актуально при огромном количестве взаимозависимых параметров). Некоторые примеры.

Реализация "fault-tolerant"-техники -- отслеживание "отваливания" процессоров и переброска задач между вычислителями при проблемах:
A formal approach for the synthesis and implementation of fault-tolerant industrial embedded systems

Применение для FPGA:
Autonomic Management of Reconfigurable Embedded Systems using Discrete Control: Application to FPGA

А это пример уже за рамками embedded -- учебный примерчик Java-серверов (синтезируемый Lustre-код может быть скомпилирован в Java) как "сервис новостей" -- переключение режимов работы распределенной системы в зависимости от сетевой нагрузки, политики организации ресурсов и пр.:
Behavioural Model-based Control for Autonomic Software Components

Фреймворк по ссылке выше есть развитие "Nemo":
A Domain-Specific Language for Multi-task Systems, applying Discrete Controller Synthesis


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Понедельник, 11 Декабрь, 2017 20:58 

Зарегистрирован: Вторник, 01 Март, 2011 09:34
Сообщения: 197
Откуда: Москва
PSV100 писал(а):
Насколько я понял, сертифицированные тулзы должны запускаться на определенных версиях винды, т.е. есть требования к исполнительной среде для самого компилятора и остальных инструментов. А вот конкретика целевых платформ, для которых генерируется код и прочее, не раскрыта.

Кодогенератор SCADE настраивается на целевые платформы, организации-разработчики могут купить этот САПР, который, похоже, действительно сертифицирован по 60880 (я со SCADE не работал). А сертификация уже конкретных целевых платформ - это уже головная боль их производителей, как-то так.


Вернуться к началу
 Профиль  
 
СообщениеДобавлено: Вторник, 12 Декабрь, 2017 20:51 

Зарегистрирован: Понедельник, 25 Июнь, 2012 17:26
Сообщения: 189
Со стороны так ситуация и выглядит.

В статейке про язык в SCADE (ранее здесь по ссылке) отмечено про "new challenge" в вопросах сертификации -- создание полностью формально верифицированного компилятора, по типу CompCert -- использование прувера (Coq в данном случае) для доказательства соответствия (корректности) целевого генерируемого кода исходной семантике в Lustre-коде. Первый шаг в этом направлении:
A Formally Verified Compiler for Lustre

Видать, своего головняка у них там также хватает.

Тем не менее, для IT в целом платформа даёт неплохие решения. Ранее здесь был упомянут PretC -- расширение для C по мотивам Esterel:
https://hal.inria.fr/hal-00786378/document

У этих же товарищей (причём как минимум один из авторов "светится" в самой Esterel) есть и ForeC -- в аналогичном стиле, только уже под многопоточную платформу (с реальными асинхронными процессами с раздельными исполнителями).
Презентация: http://slideplayer.com/slide/6392145/
Введение: https://hal.inria.fr/hal-00842402/document

Сохраняется семантика "синхронной" модели, что определяет независимость (условно) от диспетчера (шедулинга). Там же предлагается алгоритм для "Mixed-Criticality Systems" -- смешанное управление критически важных по времени задач и не очень (как некое развитие модели Prelude, ранее были ссылки):
http://www.bromans.com/publ/yip-et-al-2 ... cality.pdf

Рекомендую взглянуть, очень таки интересные штуки, причём далеко не только для embedded. Можно наглядно сравнить и оценить (для себя) стили построения систем: императивный и на dataflow-уравнениях. К примеру, на картинке ниже --организация конвейера в ForeC (из презентации выше), ранее здесь неоднократно были ссылки на асинхронные процессы в Heptagon, есть что пощупать, так сказать.
Вложение:
pipelining.png
pipelining.png [ 57.94 КБ | Просмотров: 20 ]


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 34 ]  На страницу Пред.  1, 2

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2017, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB