Synthesis from scenario-based specifications
Synthesis from scenario-based specifications
复制标题
DOI：
10.1016/j.jcss.2011.08.008
复制
发表时间：
2012-05
期刊：
影响因子：
--
通讯作者：
D. Harel;Itai Segall
中科院分区：
文献类型：
--
作者：
D. Harel;Itai Segall
我们考虑的问题，自动生成的反应系统的规范中给出的实时序列图（LSC）的基于ARIO的语言。我们首先扩展语言，使其更适合于合成。然后，我们将语言中给出的系统规范转换为系统和环境之间的双人游戏。通过解决这个问题，我们为系统生成了一个获胜的策略，它对应于规范的正确实现。我们还定义了两个概念的系统正确性，并显示如何每个可以合成。
We consider the problem of the automatic generation of reactive systems from specifications given in the scenario-based language of live sequence charts (LSCs). We start by extending the language so that it becomes more suitable for synthesis. We then translate a system specification given in the language into a two-player game between the system and the environment. By solving the game, we generate a winning strategy for the system, which corresponds to a correct implementation of the specification. We also define two notions of system correctness, and show how each can be synthesized.