{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:51:46Z","timestamp":1694623906836},"reference-count":15,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[1996,7,1]],"date-time":"1996-07-01T00:00:00Z","timestamp":836179200000},"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":["Form. Asp. Comput."],"published-print":{"date-parts":[[1996,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            A refinement calculus for the development of real-time systems is presented. The calculus is based upon a wide-spectrum language called TAM (the Temporal Agent Model), within which both functional and timing properties can be expressed in either abstract or concrete terms. A specification oriented semantics is given for the language. Program development is considered as a refinement process i.e. the\n            <jats:italic>calculation of<\/jats:italic>\n            a structured program from an unstructured specification. An example program is developed.\n          <\/jats:p>","DOI":"10.1007\/bf01213532","type":"journal-article","created":{"date-parts":[[2005,2,18]],"date-time":"2005-02-18T15:54:18Z","timestamp":1108742058000},"page":"408-427","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Real-time refinement in Manna and Pnueli's temporal logic"],"prefix":"10.1145","volume":"8","author":[{"given":"David","family":"Scholefield","sequence":"first","affiliation":[{"name":"Real-Time Research Group, Department of Computer Science, University of York, YO1 5DD, York, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","volume-title":"Tract 131","author":"Back R. J. R.","year":"1980"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00291051"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Barringer H. \u201cA Survey of Verification Techniques for Parallel Programs\u201d LNCS 191 Springer-Verlag. 1985.","DOI":"10.1007\/3-540-15239-3"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Back R. J. R. von Wright J. \u201cRefinement Concepts Formalised in Higher-Order Logic\u201d BCS Formal Aspects of Computing Vol 2 No. 3. 1990.","DOI":"10.1007\/BF01888227"},{"key":"e_1_2_1_2_5_2","unstructured":"The CIP Language Group \u201cThe Munich Project CIP: Voll\u201d LNCS 183 Springer-Verlag. 1985."},{"key":"e_1_2_1_2_6_2","unstructured":"Dijkstra E. \u201cA Discipline of Programming\u201d Prentice-Hall. 1976."},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Hooman J. \u201cSpecification and Compositional Verification of Real-Time Systems\u201d Ph.D. Thesis Technical University of Eindhoven. 1991.","DOI":"10.1007\/3-540-54947-1"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Koymans R. deRoever W. P. \u201cExamples of a Real-Time Temporal Logic Specification\u201d in The Analysis of Concurrent Systems LNCS 207 Springer-Verlag. 1985.","DOI":"10.1007\/3-540-16047-7_50"},{"key":"e_1_2_1_2_9_2","unstructured":"Morgan C. \u201cProgramming from Specifications\u201d Prentice-Hall International. 1990."},{"key":"e_1_2_1_2_10_2","unstructured":"Manna Z. Pnueli A. \u201cVerification of Concurrent Programs: a Temporal Proof System\u201d Technical Report Dept. Computer Science Stanford University. June 1983."},{"key":"e_1_2_1_2_11_2","unstructured":"Morgan C. Robinson K. Gardiner P. \u201cOn The Refinement Calculus\u201d Oxford University Programming Research Group Technical Report PRG-70. October 1988."},{"key":"e_1_2_1_2_12_2","unstructured":"Scholefield D. \u201cA Refinement Calculus for Real-Time Systems\u201d Department of Computer Science D.Phil. Thesis University of York. July 1992."},{"key":"e_1_2_1_2_13_2","unstructured":"Schonberg E. Shields D. \u201cFrom Prototype to Efficient Implementation: a Case Study Using SETL and C\u201d Courant Institute of Mathematical Sciences Dept. Computer Science New York University. 1985."},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90096-5"},{"issue":"5","key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","article-title":"A Calculus of Durations","volume":"40","author":"Chaochen Z.","year":"1991","journal-title":"Information Processing Letters"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01213532.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01213532\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01213532","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:26:36Z","timestamp":1641482796000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01213532"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,7]]},"references-count":15,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1996,7]]}},"alternative-id":["10.1007\/BF01213532"],"URL":"https:\/\/doi.org\/10.1007\/bf01213532","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,7]]}}}