Synthesis from scenario-based specifications

详细信息	查看全文 | 推荐本文 |

• 作者：David Harel ; ^{dharel@weizmann.ac.il} ; Itai Segall ; ^{itai.segall@weizmann.ac.il}
• 关键词：Synthesis ; Live sequence charts ; LSC ; Specification ; Scenario-based programming
• 刊名：Journal of Computer and System Sciences
• 出版年：2012
• 期刊代码：186_00220000
• 类别：et
• 出版时间：May, 2012
• 卷：78
• 期：3
• 页码：970-980
• 文件大小：598 K

摘要

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.