反应式系统的综合实现的解释和解释的挑战
The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems
摘要：
在反应式系统的形式化综合中，系统的实现是从其形式化规范自动构造的。综合的最大优点是，最终实现是正确的建设;因此，不需要手动编程和繁琐的调试任务。然而，开发人员仍然对使用自动合成工具犹豫不决，仍然倾向于手动编写代码。反对综合的一个共同论点是，最终的执行情况并不总是清楚地说明在综合过程中作出了哪些决定。合成工具的结果大多是不可读的，并且阻碍了开发人员理解最终实现的功能。在过去几年中，为了使综合过程对用户更加透明，进行了许多尝试。通过构建合成工具的结果，或者通过提供额外的自动化支持来帮助用户进行规范过程。在本文中，我们将讨论的挑战，在编写规范的反应系统，并给出了一个调查什么工具已经开发出来，以指导用户在指定反应系统和理解的结果合成工具。
英文摘要：
In formal synthesis of reactive systems an implementation of a system is automatically constructed from its formal specification. The great advantage of synthesis is that the resulting implementation is correct by construction; therefore there is no need for manual programming and tedious debugging tasks. Developers remain, nevertheless, hesitant to using automatic synthesis tools and still favor manually writing code. A common argument against synthesis is that the resulting implementation does not always give a clear picture on what decisions were made during the synthesis process. The outcome of synthesis tools is mostly unreadable and hinders the developer from understanding the functionality of the resulting implementation. Many attempts have been made in the last years to make the synthesis process more transparent to users. Either by structuring the outcome of synthesis tools or by providing additional automated support to help users with the specification process. In this paper we discuss the challenges in writing specifications for reactive systems and give a survey on what tools have been developed to guide users in specifying reactive systems and understanding the outcome of synthesis tools.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
