Программирование для встроенных систем - статьи

       

Разработка формальной спецификации


Формальная спецификация разрабатывается средствами CTesK. В CTesK имеются два вида спецификационных функций: стимулы и реакции. В языке nesC есть два вида интерфейсных функций — команды и события.  Интерфейсные функции nesC могут быть как стимулами, так и реакциями. Действительно, команда в nesC является стимулом для поставщика интерфейса, и реакцией для пользователя интерфейса. Событие в nesC является реакцией для поставщика интерфейса и стимулом для пользователя интерфейса.

Следующее отличие SeC от nesC заключается в том, что реакции в SeC однонаправлены, соответствуют передаче данных от источника получателю. Интерфейсные функции могут иметь возвращаемые значения и обновляемые параметры (updates parameters), то есть представляют двунаправленный обмен данными. Такая ситуация проиллюстрирована на рисунке 4.

Пара реакция/стимул

Ещё одна особенность, которая отличает тестирование компонентов TinyOS от традиционных областей применения UniTesK, заключается во взаимодействии по нескольким интерфейсам. В частности, для выполнения операции на одном интерфейсе, компонент может произвести операции на одном или нескольких других интерфейсах. На рисунке 5 представлен пример: опрос значения некоторого датчика через промежуточный менеджер атрибутов, который абстрагирует детали обращения к конкретным атрибутам. Результат, возвращаемый в ответ на запрос, зависит от результатов "переговоров" менеджера атрибутов и собственно атрибута.

Взаимодействие на нескольких интерфейсах

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

Асинхронность в TinyOS

Для тогочтобы адекватно промоделировать средствами UniTesK интерфейсные функции компонентов nesC мы предлагаем разделить вызовы команд и событий nesC на две составляющие: вызов и возврат управления. При этом поток данных от окружения к целевому компоненту специфицируется как стимул, а обратный поток данных – как реакция.


Данное решение позволяет единообразно моделировать расщеплённые операции и операции, которые возвращают управление немедленно.

Большинство компонентов TinyOS не связано с аппаратурой, поэтому все стимулы и реакции таких компонентов состоят из вызовов интерфейсных методов. По другому обстоят дела с компонентами, которые непосредственно взаимодействуют с аппаратурой. Для таких компонентов имеются непроцедурные стимулы — прерывания аппаратуры, и непроцедурные реакции — операции с "железом".

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

  • ввести спецификационные функции-реакции, которые соответствуют обращению   программного обеспечения к определённым аппаратным функциям;


  • включить модель состояния аппаратуры и представить изменения состояния аппаратуры в постусловии.


Первая стратегия применима в тех ситуациях, когда возможно перехватывать обращения к аппаратуре. Вторая стратегия является уместной, когда есть возможность наблюдать изменения состояния аппаратуры.

Конфигурации собираются из нескольких компонентов — модулей и более мелких конфигураций. Конфигурации не содержат собственного кода, все внешние интерфейсы конфигурации реализуются в компонентах, составляющих конфигурацию. Стимулы и реакции конфигурации составляются из стимулов и реакций внешних интерфейсов конфигурации. Если в состав конфигурации входят компоненты, взаимодействующие с аппаратурой, то к стимулам и реакциям конфигурации относятся также и операции с аппаратурой. С точки зрения методики разработка спецификаций для модулей и конфигураций не различаются.


Содержание раздела