Detecting Regulatory Vulnerability in Functional Requirements Specifications
Motoshi Saeki, Haruhiko Kaiya, and Satoshi Hattori.
Proceedings of the 4th International Conference on Software
and Data Technologies
(ICSOFT2009), Vol. 1, pp. 105-114,
Sofia, Bulgaria, 26-29 Jul. 2009. INSTICC.
This paper proposes a technique to apply model checking in order to show the regulatory compliance of
requirements specifications written in use case models. We define three levels of regulatory vulnerability of a
requirements specification by the situation of its non-compliance with regulations. For automatic compliance
checking, the behavior of business processes and information systems are specified with use cases and they
are translated into finite state transition machines. By using model checker SMV, we formally verify if the
regulations that are represented with computational tree logic can be satisfied with the state machines.