Supporting formal verification of crosscutting concerns

Abstract. This paper presents an approach to formal verification of the proper-ties of systems composed of multiple crosscutting concerns. The approach mod-els concerns as sets of concurrent processes, and provides a method of compo-sition that mimics the composition operators of existing multiple-concern im-plementation languages. A case study demonstrates the composition process and shows how formal verification of different composition strategies can detect po-tential problems. We also discuss the need for a general model of concerns that can be handled by different formal languages.