Теория и принципы построения датчиков, приборов и систем
Представляем работы, доложенные на Втором международном семинаре IEEE "Интеллектуальный сбор данных и современные вычислительные системы" (The Second IEEE International Workshop on Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications — IDAACS'2003) в г. Львове, Украина, 8—10 сентября 2003 г. Семинар организован Институтом компьютерных информационных технологий академии национальной экономики, г. Тернополь, Украина, совместно с Институтом компьютерных технологий, автоматизации и метрологии Национального университета "Львовский политехник". Статьи публикуются в авторских переводах на русский язык.
Здесь представлены две из этих работ. Еще две будут опубликованы в следующем номере.
УДК 681.518
ПОДХОД К СПЕЦИФИКАЦИИ, МОДЕЛИРОВАНИЮ И ВЕРИФИКАЦИИ СПОНТАННЫХ СЕНСОРНЫХ СЕТЕЙ
В. А. Олещук (Норвегия)
Рассмотрены и проанализированы проблемы применения мето да проверки конечных моделей в целях разработки надежных и правильно функционирующих распределенных сенсорных систем. Про демонстрировано испол ьзо-вание системы Spin [1, 2] для спецификации, моделирования и анализа поведения спонтанных сенсорных сетей.
1. ВВЕДЕНИЕ
Спонтанная сенсорная сеть [3, 4] представляет собой граф, в котором узлы означают сенсоры, а ребра — беспроводные каналы связи, через которые сенсоры могут обмениваться сообщениями либо непосредственно напрямую, либо через последовательность сенсоров, расположенных в промежуточных узлах графа. Сеть сенсоров часто формируется посредством спонтанного расположения и предназначается для сбора и обработки информации. Так как по своей конструкции сенсоры являются маленькими недорогими устройствами, можно ожидать, что тысячи и даже миллионы сенсоров будут использоваться в недалеком будущем. Это повлияет на многие, если не на все аспекты нашей жизни. В качестве типичных примеров применения сенсорных сетей можно привести системы сбора критической информации с целью обнаружения и локализации очагов возгорания, мониторинг состояния окружающей среды, состояния пациентов в медицинской практике [5, 7].
Области применения сенсоров, упомянутые выше, указывают на то, что надежность и корректное функционирование систем, использующих сенсорные сети, является критическим для обеспечения безопасности, сохранения здоровья и жизни людей, принятия решений и т.п. Очевидно, что последствия некорректного поведения таких систем могут быть катастрофическими. Поэтому особенно важна разработка надежных, стабильных и безопасных решений, корректность функционирования которых доказана, особенно в ненадежной, и даже во враждебной среде. С другой стороны, для сенсорных устройств характерны такие особенности как ограниченные вычислительная мощность и память, малая пропускная способность коммуникационных кана-
лов, ограниченное время жизни и автономность источников питания. Мобильность, спонтанное размещение и размер сенсорных сетей могут требовать использования принципов самоорганизации, поддерживающих динамическую реконфигурацию работающей системы. Поэтому необходимо разработать новые алгоритмы и протоколы, специфицированные и верифицированные с учетом новых ограничений и критериев корректности, вызванных новыми областями и условиями применения.
Целью данной работы является демонстрация применимости метода проверки конечных моделей (finite model-checking) к анализу и верификации сенсорных сетей, представленных в виде динамически изменяемых графов. Наличие или отсутствие ребер в динамическом графе, связывающих два узла, моделирует установление или разрыв связи между сенсорами, расположенными в этих узлах, что, в свою очередь, определяется расстоянием между сенсорами и/или их обоюдным желанием сотрудничать.
Работа построена следующим образом. В части 2 сделаны предположения о свойствах сенсорных сетей, существенные, с нашей точки зрения, при построении содержательных моделей сетей. В части 3 дано краткое описание системы Spin, реализующей методы проверки конечных моделей и используемой в этой работе для анализа свойств сенсорных сетей. В части 4 описываются основные черты модели сенсорной сети и приводится краткое описание их спецификации на языке Promela — входном языке системы Spin. В части 5 приводится краткое описание критериев корректности, интересных в контексте этой работы, а также способы их определения в системе Spin.
2. МОДЕЛИРОВАНИЕ И СПЕЦИФИКАЦИЯ
Моделирование и анализ сенсорных сетей подразумевают наличие их формальной спецификации. Так как сети могут быть достаточно большими и сложными, построение их моделей, допускающих эффективный анализ, требует моделирования только тех свойств реальных сетей и сред их работы, которые существенны для правильной верификации интересующих нас свойств реальных систем.
Мы предполагаем, что только сенсоры, находящиеся в радиусе действия друг друга, могут обмениваться сообщениями напрямую, т.е. без посредников. В сенсорной сети сенсоры могут сотрудничать между собой с целью совместного выполнения вычислительных задач, используя входные данные, полученные как от других сенсоров сети, так и от среды, в которой они работают (как, например, в случае моделирования сбора данных о состоянии окружающей среды, таких как температура, влажность и т.п.). В общем, разумно предположить, что в сенсорной сети и сенсоры, и коммуникационные каналы ненадежны, т.е. не гарантируют правильного исполнения своих функций. Мы также предполагаем, что сенсоры в сенсорной сети в лучшем случае только частично доверяют друг другу. Конечно, даже в случае, когда две сенсорные сети не доверяют друг другу, они все еще могут быть вынуждены сотрудничать, обмениваясь частичными данными для выполнения совместных вычислений [7].
Как уже упоминалось во введении, можно моделировать сенсорную сеть как динамически изменяющийся, неориентированный граф с вершинами, представляющими сенсоры, связанные ребрами в случае, когда сенсоры могут обмениваться сообщениями. В этой работе приняты следующие общие предположения о свойствах сенсоров, представленных вершинами, и сети, представленной графом.
1. Каждый узел графа — мобильный, ненадежный, имеет уникальный идентификатор среди смежных с ним узлов. Отметим, что все известные алгоритмы предполагают наличие уникального идентификатора в сети. В то же время такое требование может показаться нереалистичным в сетях, содержащих миллионы узлов и динамически изменяющуюся конфигурацию.
2. Каналы обмена сообщениями — всегда двусторонние и ненадежные.
3. Предполагается наличие поддерживающих протоколов на более низком уровне, обеспечивающих каждый узел информацией о его смежных узлах, т.е. сенсорах, с которыми можно общаться напрямую.
При учете перечисленных выше предположений поведение такой распределенной системы может быть достаточно сложным и непредсказуемым. Для анализа поведения и свойств таких систем мы предлагаем использовать методы анализа конечных систем. В частности, в этой работе использована система Spin [2], которая позволяет анализировать системы, моделируемые как системы взаимодействующих конечных автоматов и верифицировать свойства, сформулированные в виде утверждений линейной временной логики (linear temporal logic — LTL) [6].
3. СИСТЕМА ПРОВЕРКИ МОДЕЛЕЙ SPIN
В этой части дано краткое описание системы проверки моделей Spin [1, 2], выбранной в качестве программной системы для построения моделей сенсорных сетей и изучения их свойств. Верификационные модели
в системе Spin сфокусированы на доказательстве корректности взаимодействия между процессами. Эти модели пытаются абстрагироваться, насколько это возможно, от последовательных вычислений внутри процессов. В системе Spin взаимодействие процессов можно специфицировать посредством асинхронной передачи сообщений через буферные каналы конечной емкости, посредством доступа к общим разделяемым переменным или посредством комбинации этих двух методов. Для того чтобы анализировать модель в системе Spin, она должна быть представлена на языке Promela, являющимся входным языком системы Spin. На языке Promela можно специфицировать все существенные черты распределенных асинхронных систем. В сущности, каждая модель, описанная на языке Promela, представляет собой огромный конечный автомат, поведение которого можно проанализировать в системе Spin, задавая различные свойства среды функционирования модели (как, например, потеря или дублирование сообщений в канале связи и т.п.). Язык Promela делает возможным динамическое создание взаимодействующих параллельных процессов, которые затем объединяются в единую систему посредством конечных коммуникационных каналов связи. Spin позволяет как моделирование случайного поведения, так и осуществление полной или частичной верификации системы относительно критериев корректности таких как системные инварианты или утверждения линейной временной логики.
4. МОДЕЛИРОВАНИЕ НА ЯЗЫКЕ PROMELA
В этой части представлены основные черты модели сенсорной сети, включающей в себя свойства сенсорных сетей, описанные в части 2. Показано, как эти свойства можно специфицировать на языке Promela.
Так как сенсоры являются маленькими устройствами с ограниченными ресурсами, они естественным образом моделируются как взаимодействующие конечные
proctype sensor (chan to Env, chan from Env,
chan to LM, chan from LM) {
byte X, Y do
if
:: from LM!X -> { perform activity requested by LM} :: Update LM -> to LM?X :: else ->
if
:: from Env?Y -> { perform activity based on messages received from
other sensors }
:: Update Env -> to Env!Y fi
od }
Рис. 1. Фрагмент спецификации процесса sensor на языке Promela:
переменные toEnv и fromEnv позволяют моделируемому процессу взаимодействовать со своей внешней средой; переменные toLm и fromLM позволяют обмениваться сообщениями с процессом LM (location manager)
Рис. 2. Конечный автомат, моделирующий сенсор температуры
mtype = {REQ};
proctype sensorT(chan to SN, from SN) {
byte Tempr; /* temperature */ mtype msg; do
:: fromSN?msg -> if
:: (msg == REQ) -> toSN!Tempr :: else -> skip fi
:: (Tem
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.