{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T19:21:14Z","timestamp":1742930474647,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540408284"},{"type":"electronic","value":"9783540452362"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45236-2_15","type":"book-chapter","created":{"date-parts":[[2010,6,25]],"date-time":"2010-06-25T20:08:38Z","timestamp":1277496518000},"page":"244-263","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Proving the Correctness of Simpson\u2019s 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method"],"prefix":"10.1007","author":[{"given":"Neil","family":"Henderson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,9,25]]},"reference":[{"key":"15_CR1","unstructured":"Aczel, P.: On an inference rule for parallel composition. Unpublished letter to Cliff Jones (March 1983)"},{"key":"15_CR2","series-title":"FACIT","volume-title":"Proof in VDM: Case Studies","author":"S. Angerholm","year":"1998","unstructured":"Angerholm, S., Bicarregui, J., Maharaj, S.: On the Verification of VDM Specifications and Refinement with PVS. In: Bicarregui, J.C. (ed.) Proof in VDM: Case Studies. FACIT. Springer, Heidelberg (1998)"},{"key":"15_CR3","first-page":"110","volume":"10","author":"E.A. Ashcroft","year":"1975","unstructured":"Ashcroft, E.A.: Proving assertions about parallel programs. JCSS\u00a010, 110\u2013135 (1975)","journal-title":"JCSS"},{"key":"15_CR4","unstructured":"Brooke, P., Jacob, J.L., Armstrong, J.M.: Analysis of the FourSlot Mechanism. In: Proceedings of the BCS-FACS Northern Formal Methods Workshop (1996)"},{"key":"15_CR5","unstructured":"Brooke, P.J.: A Timed Semantics for a Hierarchical Design Notation. PhD thesis, Department of Computer Science, University of York (April 1999)"},{"key":"15_CR6","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Methods","author":"W.-P. Roever de","year":"2001","unstructured":"de Roever, W.-P., et al.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science, vol.\u00a0(54). Cambridge University Press, Cambridge (2001)"},{"key":"15_CR7","unstructured":"Formal Systems (Europe) Ltd. Failures-Divergence Refinement: The FDR 2.0 User Manual (August 1996)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/3-540-45614-7_20","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"N. Henderson","year":"2002","unstructured":"Henderson, N., Paynter, S.E.: The Formal Classification and Verification of Simpson\u2019s 4-Slot Asynchronous Communication Mechanism. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 350\u2013369. Springer, Heidelberg (2002)"},{"issue":"10","key":"15_CR9","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1145\/355620.361161","volume":"17","author":"C.A.R. Hoare","year":"1974","unstructured":"Hoare, C.A.R.: Monitors: An Operating System Structuring Concept. Communications of the ACM\u00a017(10), 549\u2013557 (1974)","journal-title":"Communications of the ACM"},{"key":"15_CR10","unstructured":"Jones, C.B.: Development Methods for Computing Programs Including a Notion of Interference. PhD thesis, Oxford University Computing Laboratory (1981)"},{"key":"15_CR11","first-page":"321","volume":"83","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Specification and Design of (Parallel) Programs. Information Processing Letters\u00a083, 321\u2013331 (1983)","journal-title":"Information Processing Letters"},{"issue":"4","key":"15_CR12","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps towards a development method for interfering programs. ACM Transactions an Programming Languages and Systems\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Transactions an Programming Languages and Systems"},{"key":"15_CR13","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. International Series in Computer Science (1990)"},{"key":"15_CR14","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF01786227","volume":"1","author":"L. Lamport","year":"1986","unstructured":"Lamport, L.: On Interprocess Communication \u2013 Part 1: Basic Formalism. Distributed Computing\u00a01, 77\u201385 (1986)","journal-title":"Distributed Computing"},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/BF01786228","volume":"1","author":"L. Lamport","year":"1986","unstructured":"Lamport, L.: On Interprocess Communication \u2013 Part 2: Algorithms. Distributed Computing\u00a01, 86\u2013101 (1986)","journal-title":"Distributed Computing"},{"key":"15_CR16","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1007\/BF00263649","volume":"22","author":"T. Nipkow","year":"1986","unstructured":"Nipkow, T.: Non-Deterministic Data Types: Models and Implementations. Acta Informatica\u00a022, 629\u2013661 (1986)","journal-title":"Acta Informatica"},{"key":"15_CR17","unstructured":"Nipkow, T.: Behavioural Implementation Concepts for Nondeterministic Data Types. PhD thesis, University of Manchester (May 1987)"},{"key":"15_CR18","unstructured":"Owre, S., Shanker, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language: Version 2.3. Technical report, Computer Science Laboratory \u2013 SRI International (September 1999)"},{"key":"15_CR19","unstructured":"Owre, S., Shanker, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS System Guide: Version 2.3. Technical report, Computer Science Laboratory \u2013 SRI International (September 1999)"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Paynter, S.E., Henderson, N., Armstrong, J.M.: Ramifications of metastability in bit variables explored via Simpson\u2019s 4-slot mechanism. Submitted to FACS (January 2003)","DOI":"10.1007\/s00165-004-0042-9"},{"key":"15_CR21","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall Series in Computer Science (1998)"},{"key":"15_CR22","unstructured":"Rushby, J.: Model-Checking Simpson\u2019s Four-Slot Fully Asychronous Communication Mechanism. Technical Report Issued, Computer Science Laboratory \u2013 SRI International (July 2002)"},{"key":"15_CR23","unstructured":"Simpson, H.R.: Fully Asynchronous Communication. In: Proceedings of the IEE Colloquium an MASCOT in Real-Time Systems (May 1987)"},{"issue":"1","key":"15_CR24","first-page":"17","volume":"137 Part E","author":"H.R. Simpson","year":"1990","unstructured":"Simpson, H.R.: Four-Slot Fully Asynchronous Communication Mechanism. IEE Proceedings\u00a0137 Part E(1), 17\u201330 (1990)","journal-title":"IEE Proceedings"},{"issue":"1","key":"15_CR25","first-page":"35","volume":"139 Part E","author":"H.R. Simpson","year":"1992","unstructured":"Simpson, H.R.: Correctness Analysis for Class of Asynchronous Communication Mechanism. IEE Proceedings\u00a0139 Part E(1), 35\u201349 (1992)","journal-title":"IEE Proceedings"},{"issue":"4","key":"15_CR26","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1049\/ip-cdt:19971218","volume":"144","author":"H.R. Simpson","year":"1997","unstructured":"Simpson, H.R.: New Algorithms for Asynchronous Communication. IEE Proceedings of Computer Digital Technology\u00a0144(4), 227\u2013231 (1997)","journal-title":"IEE Proceedings of Computer Digital Technology"},{"issue":"4","key":"15_CR27","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1049\/ip-cdt:19971219","volume":"144","author":"H.R. Simpson","year":"1997","unstructured":"Simpson, H.R.: Role Model Analysis of an Asynchronous Communication Mechanism. IEE Proceedings of Computer Digital Technology\u00a0144(4), 232\u2013240 (1997)","journal-title":"IEE Proceedings of Computer Digital Technology"},{"key":"15_CR28","unstructured":"Xia, F.: Supporting the MASCOT method with Petri net techniques for real- time systems development. PhD thesis, London University, King\u2019s College (January 2000)"},{"key":"15_CR29","unstructured":"Xia, F., Clark, I.: Complementing the role model method with petri-net techniques in studying issues of data freshness of the four slot mechanism. Technical Report CS-TR-654, Department of Computing Science, University of Newcastle (January 1999)"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Xia, F., Yakovlev, A.V., Clark, I.G., Shang, D.: Data communication in systems with heterogeneous timing. IEEE Micro\u00a022(6) (November- December 2002)","DOI":"10.1109\/MM.2002.1134344"}],"container-title":["Lecture Notes in Computer Science","FME 2003: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45236-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,23]],"date-time":"2020-01-23T13:08:51Z","timestamp":1579784931000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45236-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540408284","9783540452362"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45236-2_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"25 September 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}