Supporting Formal Verification of Crosscutting Concerns
Supporting Formal Verification of Crosscutting Concerns
复制标题
DOI：
10.1007/3-540-45429-2_12
复制
发表时间：
2001-09
期刊：
影响因子：
--
通讯作者：
T. Nelson;D. Cowan;P. Alencar
中科院分区：
文献类型：
--
作者：
T. Nelson;D. Cowan;P. Alencar
本文提出了一种形式化验证由多个横切关注点组成的系统属性的方法。该方法将关注点建模为并发进程集，并提供了一种模仿现有多关注点实现语言的合成操作符的合成方法。一个案例研究演示了写作过程，并展示了不同写作策略的正式验证如何发现潜在的问题。我们还讨论了对可由不同形式语言处理的关注点的通用模型的需求。
This paper presents an approach to formal verification of the properties of systems composed of multiple crosscutting concerns. The approach models concerns as sets of concurrent processes, and provides a method of composition that mimics the composition operators of existing multiple-concern implementation languages. A case study demonstrates the composition process and shows how formal verification of different composition strategies can detect potential problems. We also discuss the need for a general model of concerns that can be handled by different formal languages.