{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:08:07Z","timestamp":1725484087132},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540411864"},{"type":"electronic","value":"9783540408918"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40891-6_17","type":"book-chapter","created":{"date-parts":[[2007,5,27]],"date-time":"2007-05-27T00:01:38Z","timestamp":1180224098000},"page":"187-197","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Methods Case Study: Using Light-Weight VDM for the Development of a Security System Module"],"prefix":"10.1007","author":[{"given":"Georg","family":"Droschl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Walter","family":"Kuhn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerald","family":"Sonneck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Thuswald","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"17_CR2","unstructured":"J.-R. Abrial. System study: Method and example. Unpublished, 1999."},{"key":"17_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"METEOR: A successful application of B in a large project","author":"P. Behm","year":"1999","unstructured":"P. Behm, P. Benoit, A. Faivre, and J.-M. Meynadier. METEOR: A successful application of B in a large project. In J. M. Wing, J. Woodcock, and J. Davies, editors, Proceedings of FM\u201999 \u2014 Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, number 1708\/1709 in Lecture Notes in Computer Science, pages 369\u2013387. Springer-Verlag, 1999."},{"key":"17_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/3-540-60973-3_80","volume-title":"FME\u201996: Industrial Benefit and Advances in Formal Methods","author":"J. Bicarregui","year":"1996","unstructured":"J. Bicarregui, J. Dick, and E. Woods. Quantitative analysis of an application of formal methods. In M.-C. Gaudel and J. Woodcock, editors, FME\u201996: Industrial Benefit and Advances in Formal Methods, volume 1051 of Lecture Notes in Computer Science, pages 60-?? Springer-Verlag, 1996."},{"key":"17_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1007\/3-540-60973-3_89","volume-title":"Formal and informal specifications of a secure system component: Final results in a comparative study","author":"T. M. Brookes","year":"1996","unstructured":"T. M. Brookes, J. S. Fitzgerald, and P. G. Larsen. Formal and informal specifications of a secure system component: Final results in a comparative study. volume 1051 of Lecture Notes in Computer Science, pages 214-?? Springer-Verlag, 1996."},{"issue":"4","key":"17_CR6","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1109\/2.375178","volume":"28","author":"J. P. Bowen","year":"1995","unstructured":"J. P. Bowen and M. G. Hinchey. Ten commandments of formal methods. Computer, 28(4):56\u201363, April 1995.","journal-title":"Computer"},{"issue":"1","key":"17_CR7","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1109\/MS.1994.1279941","volume":"11","author":"D. Craigen","year":"1994","unstructured":"D. Craigen, S. Gerhart, and T. Ralston. Case study: Paris Metro signaling system. IEEE Software, 11(1):32\u201335, January 1994.","journal-title":"IEEE Software"},{"key":"17_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"1511","DOI":"10.1007\/3-540-48118-4_30","volume-title":"Lessons from the application of formal methods to the design of a storm surge barrier control system","author":"M. Chaudron","year":"1999","unstructured":"M. Chaudron, J. Tretmans, and K. Wijbrans. Lessons from the application of formal methods to the design of a storm surge barrier control system. In J. M. Wing, J. Woodcock, and J. Davies, editors, Proceedings of FM\u201999 \u2014Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, number nu1708\/1709 in Lecture Notes in Computer Science, pages 1511\u20131526. Springer-Verlag, 1999."},{"key":"17_CR9","volume-title":"The specification and verification of an access control system using the LPV technology","author":"S. Dellacherie","year":"1999","unstructured":"S. Dellacherie. The specification and verification of an access control system using the LPV technology. PhD thesis, University of Caen, France, 1999."},{"key":"17_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/3-540-63533-5_12","volume-title":"PICGAL: Practical use of formal specification to develop a complexcrit ical system","author":"L. Devauchelle","year":"1997","unstructured":"L. Devauchelle, P. G. Larsen, and H. Voss. PICGAL: Practical use of formal specification to develop a complexcrit ical system. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, FME\u201997: Industrial Applications and Strengthened Foundations of Formal Methods. Proc. 4th Intl. Symposium of Formal Methods Europe, Graz, Austria, September 1997, volume 1313 of Lecture Notes in Computer Science, pages 221-?? Springer-Verlag, 1997."},{"key":"17_CR11","unstructured":"E. H. D\u00fcrr, N. Plat, and M. de Boer. CombiCom: Tracking and tracing rail traffic using VDM++. In M. G. Hinchey and J. P. Bowen, editors, Applications of Formal Methods, Series in Computer Science, pages 203\u2013226. Prentice Hall, 1995."},{"key":"17_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Analyzing the requirements of an access control using VDMTools and PVS (abstract)","author":"G. Droschl","year":"1999","unstructured":"G. Droschl. Analyzing the requirements of an access control using VDMTools and PVS (abstract). In Proceedings of FM\u201999, number 1708\/1709 in Lecture Notes in Computer Science. Springer-Verlag, September 1999."},{"key":"17_CR13","unstructured":"G. Droschl. Design and application of a test case generator for VDM-SL. In Workshop Materials: VDM in Practice!, Part of FM\u201999. Springer-Verlag, September 1999."},{"key":"17_CR14","unstructured":"G. Droschl. Events and scenarios in VDM and PVS. In 3rd Irish Workshop in Formal Methods, Galway, Electronic Workshops in Computing. Springer-Verlag, July 1999."},{"key":"17_CR15","unstructured":"G. Droschl. Using PVS for requirements analysis of an access control. Australian Journal of Information Systems, 7(1):146\u2013157, September 1999. Special issue on Requirements Engineering."},{"key":"17_CR16","volume-title":"Formal Specification and Analysis of Requirements in Software Development","author":"G. Droschl","year":"2000","unstructured":"G. Droschl. Formal Specification and Analysis of Requirements in Software Development. PhD thesis, Institute for Software Technology, TU-Graz, Austria, April 2000. Supervisor: Peter Lucas."},{"issue":"9","key":"17_CR17","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/185009.185028","volume":"29","author":"R. Elmstr\u00f8m","year":"1994","unstructured":"R. Elmstr\u00f8m, P. G. Larsen, and P. B. Lassen. The IFAD VDM-SL toolbox: A practical approach to formal specifications. ACM SIGPLAN Notices, 29(9):77\u201380, September 1994.","journal-title":"ACM SIGPLAN Notices"},{"key":"17_CR18","unstructured":"J. Fitzgerald and P. G. Larsen. Modelling Systems \u2014 Practical Tools and Techniques in Software Development. Cambridge University Press, 1998."},{"key":"17_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"588","DOI":"10.1007\/3-540-54834-3_34","volume-title":"CICS project report: Experiences and results from the use of Z in IBM","author":"I. Houston","year":"1991","unstructured":"I. Houston and S. King. CICS project report: Experiences and results from the use of Z in IBM. volume 551 of Lecture Notes in Computer Science, pages 588-?? Springer-Verlag, 1991."},{"key":"17_CR20","unstructured":"C. B. Jones. Systematic Software Development Using VDM. Prentice-Hall International, second edition, 1990."},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"W. Kuhn and E. Schoitsch. Dependability of scaleable, distributed systems: Communication strategies for redundant processes. In Proceedings of Safecomp\u201993, Poznan, Poland. Springer-Verlag, 1993.","DOI":"10.1007\/978-1-4471-2061-2_26"},{"issue":"8","key":"17_CR22","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/142137.142153","volume":"27","author":"N. Plat","year":"1992","unstructured":"N. Plat and P. G. Larsen. An overview of the ISO\/VDM-SL standard. Sigplan Notices, 27(8):76\u201382, August 1992.","journal-title":"Sigplan Notices"},{"key":"17_CR23","unstructured":"M. Spivey. Introducing Z: A Specification Language and its Formal Semantics. Cambridge University Press, 1988."}],"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-40891-6_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T23:46:10Z","timestamp":1550360770000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40891-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540411864","9783540408918"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-40891-6_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}