Abstract
Nowadays, regulatory compliance is one of the most important issues in Japan. Due to the increasing number of regulations, it will not be easy to ensure that all governance requirements are fulfilled by the business processes of an information system. In this paper, we propose a new method of strengthening the compliance controls in information systems using model checking. We formulate an information system as a timed automaton and compliance requirements as CTL formulas. We employ the model checker UPPAAL to check whether the automaton satisfies the requirements. We apply our method to an example taken from Japanese banking regulations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Gramm-Leach-Bliley Act of 1999 (GLBA), Public Law 106-102 (113 Statute 1338). United States Senate Committee on Banking Housing and Urban Affairs (1999)
Sarbanes-Oxley Act of 2002, Public Law 107-204 (116 Statute 745). United States Senate and House of Representatives in Congress (2002)
USA Patriot Act of 2001, Public Law 107-56, HR 3162 RDS. United States Senate and House of Representatives in Congress (2001)
The Financial Instruments and Exchange Law. Financial Services Agency, The Japanese Government (2006)
Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional (2003)
Pattersson, P., Larsen, K.: UPPAAL 2k. Bulletin of the European Association for Theoretical Computer Science 70, 40–44 (2000)
Ravn, A.P., Srba, J., Vighio, S.: Modelling and Verification of Web Services Business Activity Protocol. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 357–371. Springer, Heidelberg (2011)
Iversen, T., Kristoffersen, K., Larsen, K., Laursen, M., Madsen, G., Mortensen, S., Pettersson, P., Thomasen, C.: Model-checking Real-time Control Prgorams. In: Proceedings of the 12th Euromicro Conference on Real-time Systems (ECRTS 2000), pp. 145–155 (2000)
Liu, Y., Müller, S., Xu, K.: A static compliance-checking framework for business process models. IBM System Journal 46(2) (2007)
Act on Prevention of Transfer of Criminal Proceeds, Act No. 22 of 2007. The Japanese Government (2007)
Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Schneider, F.: Enforceable security policies. ACM Transactions on Information and System Security 3(1), 30–50 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nishizaki, Sy., Ohata, T. (2013). Real-Time Model Checking for Regulatory Compliance. In: Das, V.V., Chaba, Y. (eds) Mobile Communication and Power Engineering. AIM 2012. Communications in Computer and Information Science, vol 296. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35864-7_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-35864-7_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35863-0
Online ISBN: 978-3-642-35864-7
eBook Packages: Computer ScienceComputer Science (R0)