{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,14]],"date-time":"2023-02-14T21:29:56Z","timestamp":1676410196208},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2012,5,1]],"date-time":"2012-05-01T00:00:00Z","timestamp":1335830400000},"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":[[2012,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Formal specification languages such as Z, B and VDM are used in the incremental development of abstract specifications (suitable for establishing required properties) to more concrete specifications (resembling the final implementation). This incremental development process, known as\n            <jats:italic>refinement<\/jats:italic>\n            , preserves all observable properties of the original abstract specification. Recent research has looked at applying temporal-logic model checking to such specification languages. While this assists in the establishment of properties of the abstract specification, temporal-logic properties typically refer to state variables which are regarded as non-observable. Hence, such properties are not guaranteed to be preserved by refinement. This paper investigates the classes of temporal-logic properties which are preserved by refinement, and for some of those properties that are not preserved in general, the restrictions on the refinement process under which they are preserved. Results are presented for the temporal logics LTL, CTL and the\u00a0\n            <jats:italic>\u03bc<\/jats:italic>\n            -calculus and the formal specification language Z. They apply equally, however, to related formal specification languages such as B and VDM.\n          <\/jats:p>","DOI":"10.1007\/s00165-011-0177-4","type":"journal-article","created":{"date-parts":[[2011,5,24]],"date-time":"2011-05-24T17:36:23Z","timestamp":1306258583000},"page":"393-416","source":"Crossref","is-referenced-by-count":8,"title":["Temporal-logic property preservation under Z refinement"],"prefix":"10.1145","volume":"24","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Sheffield, Sheffield, UK"}]},{"given":"Graeme","family":"Smith","sequence":"additional","affiliation":[{"name":"School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Brisbane, Australia"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0081-x"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044482830-9\/50022-9"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Derrick J Boiten E (2001) Refinement in Z and Object-Z. Foundations and advanced applications. Springer New York","DOI":"10.1007\/978-1-4471-0257-1"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0007-4"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264365"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"de Roever W-P Engelhardt K (1998) Data refinement: model-oriented proof methods and their comparison. CUP","DOI":"10.1017\/CBO9780511663079"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/244795.244800"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90113-0"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Darlot C Julliand J Kouchnarenko O (2003) Refinement preserves PLTL properties. In: Bert D Bowen J King S Wald\u00e9n M (eds) International conference of Z and B users (ZB 2003). LNCS vol 2651. Springer New York pp 408\u2013420","DOI":"10.1007\/3-540-44880-2_24"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Derrick J North S Simons A (2006) Issues in implementing a model checker for Z. In: Lui Z He J (eds) International conference on formal engineering methods (ICFEM 2006). LNCS vol 4260. Springer New York pp 678\u2013696","DOI":"10.1007\/11901433_37"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Derrick J North S Simons A (2008) Z2SAL\u2014building a model checker for Z. In: B\u00f6rger E Butler M Bowen J Boca P (eds) Abstract state machines B and Z (ABZ 2008). LNCS vol 5238. Springer New York pp 280\u2013293","DOI":"10.1007\/978-3-540-87603-8_22"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Emerson EA (1990) Temporal and modal logic. In: van Leeuwen J (ed) Handbook of theoretical computer science vol B. Elsevier Amsterdam pp 996\u20131072.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01212407"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"He J Hoare CAR Sanders JW (1986) Data refinement refined. In: European symposium on programming (ESOP \u201986). Springer New York pp 187\u2013196","DOI":"10.1007\/3-540-16442-1_14"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(87)90224-9"},{"key":"#cr-split#-e_1_2_1_2_18_2.1","doi-asserted-by":"crossref","unstructured":"Huth M Jagadeesan R Schmidt D (2001) Modal transition systems: a foundation for three-valued program analysis. In: Sands D","DOI":"10.1007\/3-540-45309-1_11"},{"key":"#cr-split#-e_1_2_1_2_18_2.2","unstructured":"(ed) 10th European symposium on programming (ESOP 2001). LNCS vol 2028 pp 155-169"},{"key":"e_1_2_1_2_19_2","unstructured":"Jones CB (1990) Systematic software development using VDM. Prentice Hall Upper Saddle River"},{"key":"e_1_2_1_2_20_2","volume-title":"Mathematical logic","author":"Kleene SC","year":"2002"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Kesten Y Manna Z Pnueli A (1994) Temporal verification of simulation and refinement. In: A decade of concurrency reflections and perspectives REX School\/symposium. Springer London pp 273\u2013346","DOI":"10.1007\/3-540-58043-3_22"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384313"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Leuschel M Massart T Currie A (2001) How to make FDR Spin: LTL model checking of CSP using refinement. In: Oliviera JN Zave P (eds) Formal methods Europe (FME 2001). LNCS vol 2021. Springer New York pp 99\u2013118","DOI":"10.1007\/3-540-45251-6_6"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Park D (1981) Concurrency and automata on infinite sequences. In: Deussen P (ed) 5th GI conference on theoretical computer science. LNCS vol 104. Springer New York pp 167\u2013183","DOI":"10.1007\/BFb0017309"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Smith G Derrick J (2004) Linear temporal logic and Z refinement. In: Rattray C Maharaj S (eds) Algebraic methodology and software technology (AMAST 2004). LNCS vol 3116. Springer New York pp 117\u2013131","DOI":"10.1007\/978-3-540-27815-3_13"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Smith G (2000) The Object-Z specification language. Advances in formal methods. Kluwer Dordrecht","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"e_1_2_1_2_31_2","unstructured":"Spivey JM (1992) The Z notation: a reference manual 2nd edn. Prentice Hall Upper Saddle River"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Smith G Winter K (2003) Proving temporal properties of Z specificatons using abstraction. In: Bert D Bowen J King S Wald\u00e9n M (eds) International conference of Z and B users (ZB 2003). LNCS vol 2651. Springer New York pp 260\u2013279","DOI":"10.1007\/3-540-44880-2_17"},{"key":"e_1_2_1_2_33_2","first-page":"85","volume-title":"International conference of Z and B users (ZB 2005). LNCS, vol 3455","author":"Smith G","year":"2005"},{"key":"e_1_2_1_2_34_2","first-page":"3","volume-title":"Handbook of process algebra, chap 1.","author":"van Glabbeek RJ","year":"2011"},{"key":"e_1_2_1_2_35_2","unstructured":"Woodcock JCP Davies J (1996) Using Z: specification refinement and proof. Prentice Hall Upper Saddle River"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0177-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0177-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0177-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:00:53Z","timestamp":1641484853000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0177-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,5]]},"references-count":36,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,5]]}},"alternative-id":["10.1007\/s00165-011-0177-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0177-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,5]]}}}