Message sequence charts (MSCs) are widely used in computer science to describe communication scenarios. Collections of communication scenarios are specified by graphs over MSCs, so-called message sequence graphs (MSGs). While nowadays almost all software is configurable, including communicating systems, MSGs have not yet been considered in a configurable setting. In this paper, we strive towards configurable communication scenarios by introducing featured MSGs. Following a feature-oriented approach, a configuration is given through a set of features, each encapsulating an incremental or optional unit of functionality. Verification of (featured) MSGs is challenging, since even for standard MSGs most model-checking problems are known to be undecidable. We show that model checking MSGs against action computation tree logic (aCTL) is undecidable. However, if the MSG follows the syntactic criterion of local synchronization, MSG admit a finite transition-system semantics. For MSGs as well as featured MSGs, local synchronization renders aCTL model checking decidable.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Featured Message Sequence Graphs

  • Clemens Dubslaff

摘要

Message sequence charts (MSCs) are widely used in computer science to describe communication scenarios. Collections of communication scenarios are specified by graphs over MSCs, so-called message sequence graphs (MSGs). While nowadays almost all software is configurable, including communicating systems, MSGs have not yet been considered in a configurable setting. In this paper, we strive towards configurable communication scenarios by introducing featured MSGs. Following a feature-oriented approach, a configuration is given through a set of features, each encapsulating an incremental or optional unit of functionality. Verification of (featured) MSGs is challenging, since even for standard MSGs most model-checking problems are known to be undecidable. We show that model checking MSGs against action computation tree logic (aCTL) is undecidable. However, if the MSG follows the syntactic criterion of local synchronization, MSG admit a finite transition-system semantics. For MSGs as well as featured MSGs, local synchronization renders aCTL model checking decidable.