{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:52:15Z","timestamp":1694623935015},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[1995,11,1]],"date-time":"1995-11-01T00:00:00Z","timestamp":815184000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1995,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We introduce NewThink, a specification language designed specifically for real-time safety-critical systems. NewThink is a component of an overall Orwellian development method for safety-critical systems which consists of a specification language, a programming language and a set of sound decomposition rules. In this paper, we present the syntax and semantics of NewThink. We demonstrate a relationship between timed and static specifications, which potentially allows us to continue using techniques from the static case in the timed case. We also prove that our extension for real-time is conservative, which is very much in keeping with our Orwellian philosophy.<\/jats:p>","DOI":"10.1007\/bf01211002","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T12:43:49Z","timestamp":1109335429000},"page":"704-727","source":"Crossref","is-referenced-by-count":0,"title":["A theory of Orwellian specifications with NewThink"],"prefix":"10.1145","volume":"7","author":[{"given":"Paul","family":"Mukherjee","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of London, Royal Holloway, TW20 0EX, Egham, Surrey, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victoria","family":"Stavridou","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of London, Royal Holloway, TW20 0EX, Egham, Surrey, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Andrews D.: VDM Specification Language Proto-Standard. Draft Standard ISO\/IEC JTC1\/SC22\/WG19 I-246 ISO December 1992. Document Reference IN9."},{"key":"e_1_2_1_2_2_2","unstructured":"Coombes A. and McDermid J.: Specifying Temporal Requirements of Distributed Real-Time Systems in Z. Technical Report YCS 92-176 University of York 1992."},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Currie I. F.: NewSpeak \u2014 a reliable programming language. In Chris Sennett editor High-integrity Software Computer Systems Series pages 122\u2013158. Pitman 1989.","DOI":"10.1007\/978-1-4684-5775-9_6"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Dawes J.: The VDM-SL Reference Guide . Pitman 1991.","DOI":"10.1201\/9781482267419"},{"key":"e_1_2_1_2_5_2","unstructured":"Davies J. W. and Schneider S.: A brief history of timed CSP. Technical Report PRG-96 University of Oxford 1992."},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Fidge C. J.: Specification and Verification of Real-Time Behaviour Using Z and RTL. In Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems . Springer-Verlag Lecture Notes in Computer Science 571 January 1992.","DOI":"10.1007\/3-540-55092-5_22"},{"key":"e_1_2_1_2_7_2","unstructured":"He J. and Bowen J.: Time Interval Semantics and Implementation of a Real-Time Programming Language. In Fourth EuroMicro Workshop on Real-Time Systems . IEEE Computer Press June 1992."},{"key":"e_1_2_1_2_8_2","unstructured":"Hoare C. A. R.: Communicating Sequential Processes . Prentice-Hall International 1985."},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Hooman J.: Specification and Compositional Verification of Real-Time systems . PhD thesis Eindhoven University of Technology 1991. Available as Springer-Verlag Lecture Notes in Computer Science 558.","DOI":"10.1007\/3-540-54947-1"},{"key":"e_1_2_1_2_10_2","unstructured":"Hansen K. M. Ravn A. P. and Stavridou V.: Linking fault trees to software specifications. In DRA Colloquium on Analysis of Requirements for Software Intensive Systems Malvern Worcs. May 1993."},{"key":"e_1_2_1_2_11_2","unstructured":"Hansen M. R. Zhou C.C. and Stauntrup J.: A Real-Time Duration Semantics for Circuits. In Workshop on Timing Issues in the Specification and Synthesis of Digital Systems March 1992."},{"key":"e_1_2_1_2_12_2","unstructured":"INMOS. occam 2 Reference Manual . Prentice-Hall International 1988."},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/12868.12870"},{"key":"e_1_2_1_2_14_2","unstructured":"Jones C. B.: Systematic Software Development Using VDM . Prentice-Hall International 1990."},{"issue":"8","key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","first-page":"817","DOI":"10.1109\/32.159841","article-title":"A Case-Study in Timed Refinement: A Mine Pump","volume":"18","author":"Mahoney B.","year":"1992","journal-title":"IEEE Transactions on Software Engineering"},{"key":"e_1_2_1_2_16_2","unstructured":"Middleburg C. A.: Logic and Specification: Extending VDM-SL for advanced formal specification . Chapman & Hall 1993."},{"key":"e_1_2_1_2_17_2","unstructured":"MOD. The Procurement of Safety Critical Software In Defence Equipment. Interim Standard 00-55 Issue 1 Ministry of Defence Directorate of Standardisation Kentigern House 65 Brown Street Glasgow G2 8EX. 1991."},{"key":"e_1_2_1_2_18_2","unstructured":"Morgan C. C.: Programming from Specifications . Prentice-Hall International 1990."},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1985.1662795"},{"key":"e_1_2_1_2_20_2","unstructured":"Mukherjee P.: Rules for Orwellian Decomposition. Technical Report CSR-93-13 University of Birmingham December 1993."},{"key":"e_1_2_1_2_21_2","unstructured":"Mukherjee P.: Specification and Implementation of real-time safety-critical systems . PhD thesis University of London 1993."},{"key":"e_1_2_1_2_22_2","unstructured":"Mukherjee P. and Wichmann B. A.: Single Transferable Vote: A case study of the use of VDM-SL. In C.J. Mitchell editor The Mathematics of Dependable Systems . Institute of Mathematics and its Applications Oxford University Press September 1993."},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.210306"},{"key":"e_1_2_1_2_24_2","unstructured":"Scholefield D. J.: A Refinement Calculus for Real-Time Systems . PhD thesis University of York Department of Computer Science 1992. Available as Technical Report YCST 92\/07."},{"key":"e_1_2_1_2_25_2","unstructured":"Spivey J. M.: The Z Notation: A Reference Manual . Prentice Hall International 1989."},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Skaakeb\u00e6k J. U. Ravn A. P. Rischel H. and Zhou C. C.: Specification of Embedded Real-Time Systems. In Fourth EuroMicro Workshop on Real-Time Systems . IEEE Computer Press June 1992.","DOI":"10.1109\/EMWRT.1992.637481"},{"issue":"5","key":"e_1_2_1_2_27_2","first-page":"269","article-title":"A Calculus of Durations","volume":"40","author":"Zhou C. C.","year":"1992","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\/BF01211002.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01211002\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01211002","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:25:16Z","timestamp":1641482716000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01211002"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,11]]},"references-count":27,"journal-issue":{"issue":"6","published-print":{"date-parts":[[1995,11]]}},"alternative-id":["10.1007\/BF01211002"],"URL":"https:\/\/doi.org\/10.1007\/bf01211002","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,11]]}}}