The use of formal methods to describe a financial crime analytics model

There are many examples of the utilization of formal methods for creating complete specifications of software applications. Often these are bounded in scope to the concept of a critical system. This work looks to expand the definition of critical systems to include systems that provide safety measures outside of contexts like utilities or military. The expanded definition is an exploration of the concept of financial crime detection measures and their specifications, a vital element in counter terrorism controls that highlight the movement of terrorists and their funding mechanisms. Within the context of financial crime detection systems we explore if formal methods can be used in the description of software from this industrial application. The resulting analysis of this research is the selection of a formal method for the documentation of a specific example of a financial crime model from industry. We further analyze the applicability of the selected method for industrial software development and survey industry experts to understand if formal methods has a valid place in the software development life cycle for financial crime solutions.