{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T06:12:18Z","timestamp":1747807938924,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319125671"},{"type":"electronic","value":"9783319125688"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22056-2_62","type":"book-chapter","created":{"date-parts":[[2011,7,1]],"date-time":"2011-07-01T06:02:00Z","timestamp":1309500120000},"page":"592-606","source":"Crossref","is-referenced-by-count":10,"title":["Taking into Account Functional Models in the Validation of IS Security Policies"],"prefix":"10.1007","author":[{"given":"Yves","family":"Ledru","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Akram","family":"Idani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00e9r\u00e9my","family":"Milhau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nafees","family":"Qamar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R\u00e9gine","family":"Laleau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Luc","family":"Richier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed-Amine","family":"Labiadh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"62_CR1","series-title":"Computer Security Series","volume-title":"Role-Based Access Control","author":"D.F. Ferraiolo","year":"2003","unstructured":"Ferraiolo, D.F., Kuhn, D.R., Chandramouli, R.: Role-Based Access Control. Computer Security Series. Artech House, Boston (2003)"},{"issue":"1","key":"62_CR2","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/1125808.1125810","volume":"15","author":"D.A. Basin","year":"2006","unstructured":"Basin, D.A., Doser, J., Lodderstedt, T.: Model driven security: From UML models to access control infrastructures. ACM Transaction of Software Engineering Methodology\u00a015(1), 39\u201391 (2006)","journal-title":"ACM Transaction of Software Engineering Methodology"},{"key":"62_CR3","doi-asserted-by":"crossref","unstructured":"Clark, D.D., Wilson, D.R.: A comparison of commercial and military computer security policies. In: IEEE Symposium on Security and Privacy, pp. 184\u2013195 (1987)","DOI":"10.1109\/SP.1987.10001"},{"key":"62_CR4","unstructured":"Fern\u00e1ndez, E.B.: A methodology for secure software design. In: Proc. of the Int. Conf. on Software Engineering Research and Practice, SERP 2004, pp. 130\u2013136. CSREA Press (2004)"},{"key":"62_CR5","volume-title":"Secure Systems Development with UML","author":"J. J\u00fcrjens","year":"2004","unstructured":"J\u00fcrjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2004)"},{"key":"62_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J. Abrial","year":"1996","unstructured":"Abrial, J.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"key":"62_CR7","volume-title":"The Object Constraint Language: Precise Modeling With UML","author":"J.B. Warmer","year":"1998","unstructured":"Warmer, J.B., Kleppe, A.G.: The Object Constraint Language: Precise Modeling With UML. Addison-Wesley, London (1998)"},{"issue":"1-3","key":"62_CR8","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.scico.2007.01.013","volume":"69","author":"M. Gogolla","year":"2007","unstructured":"Gogolla, M., B\u00fcttner, F., Richters, M.: USE: A UML-based specification environment for validating UML and OCL. Sci. Comput. Program.\u00a069(1-3), 27\u201334 (2007)","journal-title":"Sci. Comput. Program."},{"issue":"7","key":"62_CR9","doi-asserted-by":"publisher","first-page":"924","DOI":"10.1109\/TKDE.2008.28","volume":"20","author":"K. Sohr","year":"2008","unstructured":"Sohr, K., Drouineaud, M., Ahn, G.J., Gogolla, M.: Analyzing and managing role-based access control policies. IEEE Trans. Knowl. Data Eng.\u00a020(7), 924\u2013939 (2008)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"62_CR10","volume-title":"12th ACM Symp. on Access Control Models and Technologies","author":"G. Ahn","year":"2007","unstructured":"Ahn, G., Hu, H.: Towards realizing a formal RBAC model in real systems. In: 12th ACM Symp. on Access Control Models and Technologies. ACM Press, New York (2007)"},{"key":"62_CR11","first-page":"115","volume-title":"Proceedings of the 9th ACM Symposium on Access Control Models and Technologies","author":"I. Ray","year":"2004","unstructured":"Ray, I., Li, N., France, R.: Using UML to visualize role-based access-control constraints. In: Proceedings of the 9th ACM Symposium on Access Control Models and Technologies, pp. 115\u2013124. ACM Press, New York (2004)"},{"issue":"2","key":"62_CR12","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: A Lightweight Object Modelling Notation. ACM Trans. Softw. Eng. Methodol.\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"62_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/978-3-642-11811-1_31","volume-title":"Abstract State Machines, Alloy, B and Z","author":"D. Power","year":"2010","unstructured":"Power, D., Slaymaker, M., Simpson, A.: On the modelling and analysis of amazon web services access policies. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol.\u00a05977, pp. 394\u2013394. Springer, Heidelberg (2010)"},{"key":"62_CR14","unstructured":"Zao, J., Wee, H., Chu, J., Jackson, D.: RBAC Schema Verification Using Lightweight Formal Model and Constraint Analysis. In: Proceedings of 8th ACM Symposium on Access Control Models and Technologies (2003)"},{"key":"62_CR15","volume-title":"Proc. of 7th SACMAT","author":"A. Schaad","year":"2002","unstructured":"Schaad, A., Moffett, J.D.: A lightweight approach to specification and analysis of role-based access control extensions. In: Proc. of 7th SACMAT. ACM Press, New York (2002)"},{"key":"62_CR16","volume-title":"Int. Conf. on Engineering Complex Computer Systems","author":"L. Yu","year":"2009","unstructured":"Yu, L., France, R., Ray, I., Ghosh, S.: A Rigorous Approach to Uncovering Security Policy Violations in UML Designs. In: Int. Conf. on Engineering Complex Computer Systems. IEEE, Los Alamitos (2009)"},{"key":"62_CR17","volume-title":"14th ACM Symp. on Access Control Models and Technologies, SACMAT 2009","author":"M. Toahchoodee","year":"2009","unstructured":"Toahchoodee, M., Ray, I., Anastasakis, K., Georg, G., Bordbar, B.: Ensuring spatio-temporal access control for real-world applications. In: 14th ACM Symp. on Access Control Models and Technologies, SACMAT 2009. ACM, New York (2009)"},{"issue":"5","key":"62_CR18","doi-asserted-by":"publisher","first-page":"815","DOI":"10.1016\/j.infsof.2008.05.011","volume":"51","author":"D.A. Basin","year":"2009","unstructured":"Basin, D.A., Clavel, M., Doser, J., Egea, M.: Automated analysis of security-design models. Information & Software Technology\u00a051(5), 815\u2013831 (2009)","journal-title":"Information & Software Technology"},{"key":"62_CR19","unstructured":"Autrel, F., Cuppens, F., Cuppens-Boulahia, N., Coma-Brebel, C.: MotOrBAC 2: a security policy tool. In: SARSSI 2008: 3e Conf. sur la S\u00e9curit\u00e9 des Architectures R\u00e9seaux et des Syst\u00e8mes d\u2019Information, (T\u00e9l\u00e9com Bretagne) (2008)"},{"key":"62_CR20","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.infsof.2005.05.002","volume":"48","author":"A. Mammar","year":"2006","unstructured":"Mammar, A., Laleau, R.: From a B formal specification to an executable code: application to the relational database domain. Inf. Softw. Technol.\u00a048, 253\u2013279 (2006)","journal-title":"Inf. Softw. Technol."},{"issue":"1","key":"62_CR21","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C. Snook","year":"2006","unstructured":"Snook, C., Butler, M.: UML-B: Formal modeling and design aided by UML. ACM Transactions on Software Engineering Methodology\u00a015(1), 92\u2013122 (2006)","journal-title":"ACM Transactions on Software Engineering Methodology"},{"issue":"2","key":"62_CR22","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M. Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT\u00a010(2), 185\u2013203 (2008)","journal-title":"STTT"},{"issue":"3","key":"62_CR23","doi-asserted-by":"publisher","first-page":"87","DOI":"10.3166\/isi.15.3.87-112","volume":"15","author":"A. Idani","year":"2010","unstructured":"Idani, A., Labiadh, M.A., Ledru, Y.: Infrastructure dirig\u00e9e par les mod\u00e8les pour une int\u00e9gration adaptable et \u00e9volutive de UML et B. Ing\u00e9nierie des Syst\u00e8mes d\u2019Information\u00a015(3), 87\u2013112 (2010)","journal-title":"Ing\u00e9nierie des Syst\u00e8mes d\u2019Information"},{"key":"62_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-540-30142-4_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wildmoser","year":"2004","unstructured":"Wildmoser, M., Nipkow, T.: Certifying Machine Code Safety: Shallow versus Deep Embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 305\u2013320. Springer, Heidelberg (2004)"},{"issue":"2","key":"62_CR25","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s10270-003-0024-z","volume":"2","author":"M. Frappier","year":"2003","unstructured":"Frappier, M., St-Denis, R.: EB 3: an entity-based black-box specification method for information systems. Software and Systems Modeling\u00a02(2), 134\u2013149 (2003)","journal-title":"Software and Systems Modeling"},{"key":"62_CR26","volume-title":"CSP\u2013Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: CSP\u2013Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)"},{"issue":"3","key":"62_CR27","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/s11334-008-0064-1","volume":"4","author":"M. Frappier","year":"2008","unstructured":"Frappier, M., Gervais, F., Laleau, R., Fraikin, B., St-Denis, R.: Extending statecharts with process algebra operators. Innovations in Systems and Software Engineering\u00a04(3), 285\u2013292 (2008)","journal-title":"Innovations in Systems and Software Engineering"},{"issue":"3","key":"62_CR28","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming\u00a08(3), 231\u2013274 (1987)","journal-title":"Science of Computer Programming"},{"key":"62_CR29","unstructured":"Frappier, M., Gervais, F., Laleau, R., Fraikin, B.: Algebraic state transition diagrams. Technical Report\u00a024, Universit\u00e9 de Sherbrooke, D\u00e9partement d\u2019informatique, Sherbrooke, Qu\u00e9bec, Canada (June 2008)"},{"key":"62_CR30","unstructured":"Salabert, K., Milhau, J., et al.: iASTD: un interpr\u00e9teur pour les ASTD. In: AFADL 2010, Poitiers, France (2010)"},{"key":"62_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-16265-7_18","volume-title":"Integrated Formal Methods","author":"J. Milhau","year":"2010","unstructured":"Milhau, J., Frappier, M., Gervais, F., Laleau, R.: Systematic translation rules from astd to event-B. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol.\u00a06396, pp. 245\u2013259. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Progress in Pattern Recognition, Image Analysis, Computer Vision, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22056-2_62","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,29]],"date-time":"2019-03-29T14:13:48Z","timestamp":1553868828000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22056-2_62"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783319125671","9783319125688"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22056-2_62","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}