Petri-net Analyzer验证面向方面活动图的横切属性

"这篇研究论文探讨了如何使用Petri-net Analyzer工具来验证面向方面的活动图，特别是针对横切属性的正确性。论文作者包括Zhanqi Cui、Linzhang Wang、Xi Liu、Lei Bu、Jianhua Zhao、Xuandong Li，他们来自南京大学的新软件技术国家重点实验室。该工作提出了一种框架，利用Petri网验证技术对集成的面向方面UML活动图进行验证，旨在在实施前发现可能违反系统所需属性的潜在错误。" 面向方面的编程(AOP)是一种软件开发方法，它旨在解决横切关注点（如日志、安全性和事务管理）的模块化问题，这些关注点通常会贯穿于系统的多个部分。在设计阶段，面向方面的模型驱动方法被用来建模和整合这些横切关注点，但仍然有可能在过程中引入违反系统期望属性的潜在错误。 活动图是UML（统一建模语言）中的一种图形表示，用于描述系统的动态行为，尤其是业务流程或工作流。当与面向方面的编程结合时，活动图可以表示横切属性如何影响主流程。 Petri网是一种数学模型，常用于并发系统和分布式系统的建模和分析。它们提供了一种直观的方式来表示系统状态的变化和转换，特别适合于验证系统的正确性和一致性。在这篇论文中，作者将集成的面向方面的活动图转换成Petri网，然后通过形式化的横切需求来检查这些Petri网，以此来检测可能的错误。 论文的主要贡献在于提供了一个验证框架，该框架结合了面向方面的编程和Petri网验证技术。这个框架允许开发者在设计阶段就对模型进行验证，从而早期发现和修复设计问题，提高软件质量。通过这种方式，可以确保模型符合预定义的横切属性，减少潜在的错误引入，提升软件系统的可靠性。 这篇研究论文为面向方面的软件开发提供了一个强大的验证工具，通过Petri-net Analyzer对活动图的验证，可以在设计阶段就对横切属性的正确性进行评估，这对于提高软件工程的效率和软件产品的质量具有重要意义。