面向特征编程范式的形式化验证技术研究综述

A Survey on the Formal Verification of Feature-Oriented Programming

以面向对象编程范式开发软件经常面临类(Class)与用户需求项无法直接对应的尴尬,面向特征编程范式(FOP)旨在解决这个问题,因此具有重要意义。本文首先简介了FOP编程范式的思想,它与面向方面编程范式的异同,以及它给相应的形式化验证技术带来的挑战;然后综述了现有的FOP形式化验证方法以及我们所做的相关工作,比较了它们的优缺点;最后讨论了FOP形式化验证今后可能的研究方向。

It is often not so easy to map the classes directly to the user requirements when developing with the Object-Oriented methodology. Feature-Oriented Programming methodology can solve this problem,so it has significant meaning. In this paper,we firstly introduce the ideas of FOP,its similarities and differences with Aspect-Oriented Programming,and its influence on the corresponding formal verification methods; then we survey the existing FOP formal verification methods and our related work,compare their advantages and disadvantages.Finally,we prospect the future directions of formal verification on FOP.