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.
翻译:Petri网迫使我们说什么:比较行为组合方法
翻译后的摘要:
我们确定和证明了Petri网(PN)在指定反应性系统复合行为方面的一个弱点。具体来说,我们展示了在一个PN模型中指定多个要求时,模型师被迫指定将这些要求组合的机制。这在许多情况下导致了过度规范和不正确的模型。我们演示了如何忽略某些执行路径,以及无意中生成某些执行路径。为了支持这一说法,我们分析了来自文献的PN模型,识别了组合机制,并展示了它们对模型正确性的影响。为了解决这个问题,我们提出使用行为编程(BP)对系统行为进行建模,这是一种设计用于无缝集成独立需求的软件开发和建模范式。具体来说,我们演示了BP的语义,这些语义定义了如何将场景编织到单个模型中,从而避免了过度规范。此外,尽管BP保持了与PN相同的数学属性,但它提供了改变模型动态性的手段,从而增加了规范的灵活性。我们通过分析模型、其生成的执行路径和规范过程,比较BP和PN在定量和定性上的性能。最后,尽管BP的工具支持应用形式化方法和推理技术来处理模型,但它缺乏PN工具和算法的遗产。为了解决这个问题,我们提出了BP模型到PN和反之互相转换的语义和工具。