Guided Synthesis of Control Programs Using UPPAAL
Guided Synthesis of Control Programs Using UPPAAL
复制标题
使用 UPPAAL 引导合成控制程序
DOI：
--
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
P. Pettersson
中科院分区：
文献类型：
--
作者：
T. Hune;K. Larsen;P. Pettersson
在本文中，我们解决的问题，调度和综合分布式控制程序的批量生产工厂。我们使用一个时间自动机模型的批处理厂和验证工具UPPAAL来解决调度问题。在建模的工厂，我们的目标是在一个抽象的水平，这是足够准确的，以便合成的控制程序从生成的时间轨迹是可能的。因此，模型很快变得过于详细和复杂，无法立即自动合成。事实上，只有生产两批的工厂模型才能直接分析！为了克服这个问题，我们提出了一个通用的方法，允许用户指导的模型检查器根据具体选择的策略。通过用额外的制导变量扩充模型，并通过在这些变量上用额外的保护来装饰过渡，来指定制导。应用该方法，对一个生产60批的工厂进行了控制程序的综合，并在实际工厂中得到了执行。除了在验证工厂模型和发现一些建模错误方面证明有用之外，我们还将这最后一步视为我们的方法从基本工厂模型生成可执行（和执行）代码的能力的最终试金石。
In this paper we address the problem of scheduling and synthesizing distributed control programs for a batch production plant. We use a timed automata model of the batch plant and the verification tool UPPAAL to solve the scheduling problem.In modeling the plant, we aim at a level of abstraction which is sufficiently accurate in order that synthesis of control programs from generated timed traces is possible. Consequently, the models quickly become too detailed and complicated for immediate automatic synthesis. In fact, only models of plants producing two batches can be analyzed directly! To overcome this problem, we present a general method allowing the user to guide the model-checker according to heuristically chosen strategies. The guidance is specified by augmenting the model with additional guidance variables and by decorating transitions with extra guards on these. Applying this method have made synthesis of control programs feasible for a plant producing as many as 60 batches.The synthesized control programs have been executed in a physical plant. Besides proving useful in validating the plant model and in finding some modeling errors, we view this final step as the ultimate litmus test of our methodology's ability to generate executable (and executing) code from basic plant models.