{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:46:21Z","timestamp":1764402381728},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441571"},{"type":"electronic","value":"9783540457329"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45732-1_10","type":"book-chapter","created":{"date-parts":[[2007,10,10]],"date-time":"2007-10-10T20:38:56Z","timestamp":1192048736000},"page":"82-93","source":"Crossref","is-referenced-by-count":12,"title":["Safety and Security Analysis of Object-Oriented Models"],"prefix":"10.1007","author":[{"given":"Kevin","family":"Lano","sequence":"first","affiliation":[]},{"given":"David","family":"Clark","sequence":"additional","affiliation":[]},{"given":"Kelly","family":"Androutsopoulos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,18]]},"reference":[{"key":"10_CR1","unstructured":"K. Androutsopoulos, The RSDS Tool, Department of Computer Science, King\u2019s College, 2001. http:\/\/www.dcs.kcl.ac.uk\/pg\/kelly\/Tools\/"},{"key":"10_CR2","unstructured":"Alan Dix, Janet Finlay, Gregory Abowd, Russell Beale, Human-Computer Interaction, 2nd Edition, Prentice Hall, 1998."},{"key":"10_CR3","unstructured":"ISO, Guidelines for the Use of the C Language in Vehicle Based Software, ISO TR\/15497. Also at: http:\/\/www.misra.org.uk\/ ."},{"key":"10_CR4","unstructured":"J.L. Lanet, A. Requet, Formal Proof of Smart Card Applets Correctness, Proceedings of 3rd Smart Card Research and Advanced Application Conference (CARDIS\u2019 98), Sept. 1998."},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"K. Lano, D. Clark, K. Androutsopoulos, P. Kan, Invariant-based Synthesis of Fault-tolerant Systems, FTRTFT 2000, Pune, India, 2000.","DOI":"10.1007\/3-540-45352-0_6"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"P. Lartigue, D. Sabatier, The use of the B Formal Method for the Design and Validation of the Transaction Mechanism for Smart Card Applications, Proceedings of FM\u2019 99, pp. 348\u2013368, Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48119-2_21"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Nancy G. Leveson. Designing a Requirements Specification Language for Reactive Systems. Invited talk, Z User Meeting, 1998, Springer Verlag 1998.","DOI":"10.1007\/978-3-540-49676-2_10"},{"key":"10_CR8","unstructured":"Rational Software et al, OMG Unified Modeling Language Specification Version 1.4, 2001."},{"key":"10_CR9","unstructured":"K R Leino, J Saxe, R Stata, Checking Java programs with Guarded Commands, in Formal Techniques for Java Programs, technical report 251, Fernuniversit\u00e4t Hagen, 1999."},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"R. Winther, O-A. Johansen, B.A. Gran, Security Assessments of Safety Critical Systems using HAZOPS, Safecomp 2000.","DOI":"10.1007\/3-540-45416-0_2"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45732-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T14:40:47Z","timestamp":1556894447000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45732-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441571","9783540457329"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/3-540-45732-1_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}