Detecting Regulatory Vulnerability from Use Case Models with a Model Checker

paper index | HOME

Title: Detecting Regulatory Vulnerability from Use Case Models with a Model Checker
Author(s): Motoshi Saeki, Haruhiko Kaiya and Satoshi Hattori
Source: Proceedings of the Forum at the CAiSE 2009 Conference (CAiSE 2009 Forum), pp. 13-18, 8-12 June 2009 Amsterdam, The Netherlands.

Abstract:
This paper proposes the technique to apply model checking in order to show the regulatory compliance of requirements specifications written in use case models. For automatic compliance checking, the behavior of business processes and information systems are specified with use case models and they are translated into finite state transition machines, while we represent regulations with branching time temporal logic (CTL: computational tree logic). By using model checker SMV, we formally verify if the regulations can be satisfied with the state machines.