Checking Regulatory Compliance of Business Processes and Information Systems
Motoshi Saeki, Haruhiko Kaiya, and Satoshi Hattori.
In Software and Data Technologies, Vol. 50, pp. 71-84.
Springer, 2011. Communications in Computer and Information Science (CCIS),
4th International Conference,
ICSOFT 2009, Sofia, Bulgaria, July 26-29, 2009. Revised Selected Papers.
In these years, many laws and regulations are being enacted to prevent
business processes (BPs) and information systems (ISs) from their malicious
users. As a result, it is significant for organizations to ensure that their BPs and
ISs business comply with these regulations. This paper proposes a technique to
apply a formal technique to ensure the regulatory compliance of BP or IS descriptions
written in use case models.We translate the use case models of the behavior
of BPs and ISs into finite state transition machines. Regulations are represented
with computational tree logic (CTL) and their satisfiability are automatically verified
using a model checker SMV. The modality of regulations can be specified
with temporal operators based on branching time semantics of the CTL in our