Согласование конформности и композиции.
Согласование конформности и композиции.
Авторы
Аннотация
В нашей предыдущей статье [1] предлагалась новая модель реализации типа LTS. В обычной LTS переходы помечаются действиями, поэтому еј можно назвать LTS действий. Новая модель LTS наблюдений, в ней вместо действий используются наблюдения и тестовые воздействия (кнопки). Эта модель обобщает многие семантики тестирования, которые опираются на LTS действий, но используют дополнительные наблюдения (отказы, множества готовности и т.п.). Кроме того, единообразно моделируются системы с приоритетами, которые не описываются с помощью LTS действий. В данной статье мы развиваем этот подход, концентрируя внимание на композиции систем. Дело в том, что на трассах наблюдений невозможно определить такую композицию, по отношению к которой композиция LTS обладала бы свойством аддитивности: множество трасс композиции LTS совпадает с множеством всех попарных композиций трасс LTS-операндов. Это объясняется тем, что наблюдение в композиционном состоянии не вычисляется по наблюдениям в состояниях-операндах. В данной статье мы предлагаем подход, устраняющий этот недостаток. Для этого переходы LTS помечаются такими символами (событиями), которые, с одной стороны, можно компоновать для обеспечения свойства аддитивности, а, с другой стороны, можно использовать для генерации наблюдений при тестировании: переход по событию приводит к возникновению связанного с этим событием наблюдения. Эта модель названа LTS событий. В статье определяется 1) преобразование LTS событий в LTS наблюдений для согласования с положениями нашей предыдущей статьи [1], 2) композиция LTS событий, 3) композиция спецификаций, сохраняющая конформность: композиция конформных реализаций конформна композиции спецификаций, 4) единообразное моделирование LTS действий через LTS событий, которое позволяет рассматривать реализацию в любой семантике взаимодействия, допустимой для LTS действий. При этом композиция LTS событий, полученных в результате моделирования исходных LTS действий, эквивалентна LTS событий, полученной в результате моделирования композиции этих LTS действий.
Полный текст статьи в формате pdfИздание
Программирование, 2013, №6–стр. 3-15.
Научная группа
Все публикации за 2013 год
Все публикации