Разработка формальной спецификации
Формальная спецификация разрабатывается средствами CTesK. В CTesK имеются два вида спецификационных функций: стимулы и реакции. В языке nesC есть два вида интерфейсных функций — команды и события. Интерфейсные функции nesC могут быть как стимулами, так и реакциями. Действительно, команда в nesC является стимулом для поставщика интерфейса, и реакцией для пользователя интерфейса. Событие в nesC является реакцией для поставщика интерфейса и стимулом для пользователя интерфейса.
Следующее отличие SeC от nesC заключается в том, что реакции в SeC однонаправлены, соответствуют передаче данных от источника получателю. Интерфейсные функции могут иметь возвращаемые значения и обновляемые параметры (updates parameters), то есть представляют двунаправленный обмен данными. Такая ситуация проиллюстрирована на рисунке 4.
Пара реакция/стимул
Ещё одна особенность, которая отличает тестирование компонентов TinyOS от традиционных областей применения UniTesK, заключается во взаимодействии по нескольким интерфейсам. В частности, для выполнения операции на одном интерфейсе, компонент может произвести операции на одном или нескольких других интерфейсах. На рисунке 5 представлен пример: опрос значения некоторого датчика через промежуточный менеджер атрибутов, который абстрагирует детали обращения к конкретным атрибутам. Результат, возвращаемый в ответ на запрос, зависит от результатов "переговоров" менеджера атрибутов и собственно атрибута.
Взаимодействие на нескольких интерфейсах
Специфика применения UniTesK к TinyOS связана и с асинхронным кодом. Вызов некоторой интерфейсной функции может быть прерван асинхронным вызовом, причём второй вызов может повлиять на результат первого вызова.
Асинхронность в TinyOS
Для тогочтобы адекватно промоделировать средствами UniTesK интерфейсные функции компонентов nesC мы предлагаем разделить вызовы команд и событий nesC на две составляющие: вызов и возврат управления. При этом поток данных от окружения к целевому компоненту специфицируется как стимул, а обратный поток данных – как реакция.
Данное решение позволяет единообразно моделировать расщеплённые операции и операции, которые возвращают управление немедленно.
Большинство компонентов TinyOS не связано с аппаратурой, поэтому все стимулы и реакции таких компонентов состоят из вызовов интерфейсных методов. По другому обстоят дела с компонентами, которые непосредственно взаимодействуют с аппаратурой. Для таких компонентов имеются непроцедурные стимулы — прерывания аппаратуры, и непроцедурные реакции — операции с "железом".
С точки зрения разработки формальных спецификаций компоненты, взаимодействующие с аппаратурой, ничем особенным не отличаются. Непроцедурные стимулы можно моделировать спецификационными функциями-стимулами, а для описания воздействия на аппаратуру есть две стратегии:
- ввести спецификационные функции-реакции, которые соответствуют обращению программного обеспечения к определённым аппаратным функциям;
- включить модель состояния аппаратуры и представить изменения состояния аппаратуры в постусловии.
Первая стратегия применима в тех ситуациях, когда возможно перехватывать обращения к аппаратуре. Вторая стратегия является уместной, когда есть возможность наблюдать изменения состояния аппаратуры.
Конфигурации собираются из нескольких компонентов — модулей и более мелких конфигураций. Конфигурации не содержат собственного кода, все внешние интерфейсы конфигурации реализуются в компонентах, составляющих конфигурацию. Стимулы и реакции конфигурации составляются из стимулов и реакций внешних интерфейсов конфигурации. Если в состав конфигурации входят компоненты, взаимодействующие с аппаратурой, то к стимулам и реакциям конфигурации относятся также и операции с аппаратурой. С точки зрения методики разработка спецификаций для модулей и конфигураций не различаются.
