{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T18:18:04Z","timestamp":1773080284149,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540255598","type":"print"},{"value":"9783540320074","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11415787_18","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T22:07:36Z","timestamp":1278886056000},"page":"299-318","source":"Crossref","is-referenced-by-count":16,"title":["GeneSyst: A Tool to Reason About Behavioral Aspects of B Event Specifications. Application to Security Properties"],"prefix":"10.1007","author":[{"given":"Didier","family":"Bert","sequence":"first","affiliation":[]},{"given":"Marie-Laure","family":"Potet","sequence":"additional","affiliation":[]},{"given":"Nicolas","family":"Stouls","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B Book - Assigning Programs to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B Book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"18_CR2","unstructured":"Abrial, J.-R.: Extending B without Changing it (for Developing Distributed Systems). In: Habrias, H. (ed.) First B conference, Putting into Practice Methods and Tools for Information System Design, IRIN, pp. 169\u2013191 (1996)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0053357","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"J.R. Abrial","year":"1998","unstructured":"Abrial, J.R., Mussat, L.: Introducing Dynamic Constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol.\u00a01393, pp. 83\u2013128. Springer, Heidelberg (1998)"},{"key":"18_CR4","unstructured":"Ambert, F., Bouquet, F., Chemin, S., Guenaud, S., Legeard, B., Peureux, F., Utting, M., Vacelet, N.: BZ-testing tools: A tool-set for test generation from Z and B using constraint logic programming. In: Formal Approaches to Testing of Software (FATES 2002), pp. 105\u2013120. INRIA (2002)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-40911-4_14","volume-title":"Integrated Formal Methods","author":"D. Bert","year":"2000","unstructured":"Bert, D., Cave, F.: Construction of Finite Labelled Transition Systems from B Abstract Systems. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol.\u00a01945, pp. 235\u2013254. Springer, Heidelberg (2000)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/3-540-40911-4_22","volume-title":"Integrated Formal Methods","author":"D. Cansell","year":"2000","unstructured":"Cansell, D., M\u00e9ry, D., Merz, S.: Predicate Diagrams for the Verification of Reactive Systems. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol.\u00a01945, pp. 380\u2013397. Springer, Heidelberg (2000)"},{"key":"18_CR7","unstructured":"Cansell, D., M\u00e9ry, D., Merz, S.: Diagram Refinements for the Design of Reactive Systems. Journal of Universal Computer Science\u00a07(2) (2001)"},{"key":"18_CR8","unstructured":"Common Criteria. Common Criteria for Information Technology Security Evaluation, Norme ISO 15408 - version 2.1, Aout (1999)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)"},{"key":"18_CR10","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)"},{"issue":"3","key":"18_CR11","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: A Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems\u00a016(3), 872\u2013923 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"9","key":"18_CR12","doi-asserted-by":"publisher","first-page":"768","DOI":"10.1109\/32.464544","volume":"21","author":"L. Lamport","year":"1995","unstructured":"Lamport, L.: TLA in Pictures. Software Engineering\u00a021(9), 768\u2013775 (1995)","journal-title":"Software Engineering"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/3-540-47884-1_7","volume-title":"Integrated Formal Methods","author":"H. Ledang","year":"2002","unstructured":"Ledang, H., Souqui\u00e8res, J.: Contributions for Modelling UML State-charts in B. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol.\u00a02335, pp. 109\u2013127. Springer, Heidelberg (2002)"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"18_CR15","unstructured":"Marlet, R.: DEMONEY: Java Card Implementation. Public technical report, SECSAFE project, 11 (2002)"},{"key":"18_CR16","unstructured":"Marlet, R., Mesnil, C.: DEMONEY: A demonstrative Electronic Purse - Card Specification -. Public technical report, SECSAFE project, 11 (2002)"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-45608-2_3","volume-title":"Foundations of Security Analysis and Design","author":"P. Samarati","year":"2001","unstructured":"Samarati, P., De Capitani di Vimercati, S.: Access Control: Policies, Models, and Mechanisms. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol.\u00a02171, pp. 137\u2013196. Springer, Heidelberg (2001)"},{"issue":"1","key":"18_CR18","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F.B. Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. Information and System Security\u00a03(1), 30\u201350 (2000)","journal-title":"Information and System Security"},{"key":"18_CR19","unstructured":"SecSafe. SecSafe Porject Home Page, \n                  \n                    http:\/\/www.doc.ic.ac.uk\/~siveroni\/secsafe\/"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/3-540-47884-1_8","volume-title":"Integrated Formal Methods","author":"E. Sekerinski","year":"2002","unstructured":"Sekerinski, E., Zurob, R.: Translating Statecharts to B. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol.\u00a02335, pp. 128\u2013144. Springer, Heidelberg (2002)"},{"key":"18_CR21","unstructured":"SUN. Java Card 2.1 Platform Specifications, \n                  \n                    http:\/\/java.sun.com\/products\/javacard\/specs.html"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-45719-4_23","volume-title":"Algebraic Methodology and Software Technology","author":"K. Trentelman","year":"2002","unstructured":"Trentelman, K., Huisman, M.: Extending JML Specifications with Temporal Logic. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 334\u2013348. Springer, Heidelberg (2002)"},{"key":"18_CR23","unstructured":"Voisinet, J.-C., Tatibouet, B.: Generating Statecharts from B Specifications. In: 16th Int Conf. on Software and System Engineering and their applications (ISCEA 2003), vol.\u00a01 (2003)"}],"container-title":["Lecture Notes in Computer Science","ZB 2005: Formal Specification and Development in Z and B"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11415787_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:03:43Z","timestamp":1619507023000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11415787_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255598","9783540320074"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11415787_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}