论文标题

培养皿净到什么义务我们要说:比较行为组成的方法

What Petri Net Obliges Us to Say: Comparing Approaches for Behavior Composition

论文作者

Elyasaf, Achiya, Yaacov, Tom, Weiss, Gera

论文摘要

我们在指定反应性系统的复合行为中识别并证明了培养皿(PN)的弱点。具体而言,我们展示了如何在一个PN模型中指定多个要求时,建模者有义务指定结合这些要求的机制。在许多情况下,这产生了过度指定和不正确的模型。我们演示了如何错过某些执行路径,有些是无意间生成的。为了支持这一主张,我们分析了文献中的PN模型,确定组合机制,并证明了它们对模型正确性的影响。为了解决这个问题,我们建议使用行为编程(BP)建模系统行为,这是一种软件开发和建模范式,旨在无缝集成独立要求。具体而言,我们演示了如何定义如何将场景交织成单个模型的BP的语义,允许避免过度规格。另外,尽管BP保持与PN相同的数学属性,但它提供了动态更改模型的手段,从而提高了规范的敏捷性。我们通过分析模型,生成的执行路径和规范过程来比较定量和定性措施中的BP和PN。最后,尽管BP受到允许将形式方法和推理技术应用于模型的工具的支持,但它缺乏PN工具和算法的遗产。为了解决这个问题,我们建议语义和一种将BP模型转换为PN的工具,反之亦然。

We identify and demonstrate a weakness of Petri Nets (PN) in specifying composite behavior of reactive systems. Specifically, we show how, when specifying multiple requirements in one PN model, modelers are obliged to specify mechanisms for combining these requirements. This yields, in many cases, over-specification and incorrect models. We demonstrate how some execution paths are missed, and some are generated unintentionally. To support this claim, we analyze PN models from the literature, identify the combination mechanisms, and demonstrate their effect on the correctness of the model. To address this problem, we propose to model the system behavior using behavioral programming (BP), a software development and modeling paradigm designed for seamless integration of independent requirements. Specifically, we demonstrate how the semantics of BP, which define how to interweave scenarios into a single model, allow avoiding the over-specification. Additionally, while BP maintains the same mathematical properties as PN, it provides means for changing the model dynamically, thus increasing the agility of the specification. We compare BP and PN in quantitative and qualitative measures by analyzing the models, their generated execution paths, and the specification process. Finally, while BP is supported by tools that allow for applying formal methods and reasoning techniques to the model, it lacks the legacy of PN tools and algorithms. To address this issue, we propose semantics and a tool for translating BP models to PN and vice versa.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源