论文标题
使用交替接口自动机组合部分规格
Combining Partial Specifications using Alternating Interface Automata
论文作者
论文摘要
为了建模实际软件系统，建模范例应支持一种组成性。在接口理论和基于模型的输入和输出的测试中，已经引入了连接操作员：组成规范S1 $ \ wedge $ S2允许的行为是部分模型S1和S2允许的行为。手头的模型是非确定性的界面自动机，但是非确定性和连词之间的相互作用尚未得到充分了解。另一方面，在交替的自动机理论中，连词和非确定性是核心方面。在输入和输出的背景下，尚未考虑交替的自动机，从而使它们不适合建模软件界面。在本文中，我们将两个建模范式结合在一起，以定义交替的接口自动机（AIA）。我们为这些自动机配备了观察性的基于痕量的语义，并定义了测试仪，以建立有关AIA规范的黑盒接口的正确性。
To model real-world software systems, modelling paradigms should support a form of compositionality. In interface theory and model-based testing with inputs and outputs, conjunctive operators have been introduced: the behaviour allowed by composed specification s1 $\wedge$ s2 is the behaviour allowed by both partial models s1 and s2. The models at hand are non-deterministic interface automata, but the interaction between non-determinism and conjunction is not yet well understood. On the other hand, in the theory of alternating automata, conjunction and non-determinism are core aspects. Alternating automata have not been considered in the context of inputs and outputs, making them less suitable for modelling software interfaces. In this paper, we combine the two modelling paradigms to define alternating interface automata (AIA). We equip these automata with an observational, trace-based semantics, and define testers, to establish correctness of black-box interfaces with respect to an AIA specification.
