{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T23:06:21Z","timestamp":1781651181259,"version":"3.54.5"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,3,15]],"date-time":"2015-03-15T00:00:00Z","timestamp":1426377600000},"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":["Softw Syst Model"],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1007\/s10270-015-0456-2","type":"journal-article","created":{"date-parts":[[2015,3,14]],"date-time":"2015-03-14T06:01:03Z","timestamp":1426312863000},"page":"1091-1116","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["The Unit-B method: refinement guided by progress concerns"],"prefix":"10.1007","volume":"15","author":[{"given":"Simon","family":"Hudon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thai Son","family":"Hoang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jonathan S.","family":"Ostroff","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,3,15]]},"reference":[{"key":"456_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"JR Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"456_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B\u2014System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B\u2014System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"issue":"6","key":"456_CR3","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), 447\u2013466 (2010)","journal-title":"STTT"},{"key":"456_CR4","volume-title":"Parallel program design - a foundation","author":"M Chandy","year":"1989","unstructured":"Chandy, M., Misra, J.: Parallel program design - a foundation. Addison-Wesley, Reading (1989)"},{"key":"456_CR5","doi-asserted-by":"crossref","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"456_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E Dijkstra","year":"1990","unstructured":"Dijkstra, E., Scholten, C.: Predicate Calculus and Program Semantics. Springer, New York (1990)"},{"key":"456_CR7","unstructured":"Dijkstra, E.W.: The Notational Conventions I Adopted, and Why (2000). http:\/\/www.cs.utexas.edu\/users\/EWD\/ewd13xx\/EWD1300.PDF . Circulated privately"},{"key":"456_CR8","unstructured":"Dijkstra, R.: Computation Calculus: Bridging a Formalization Gap. Mathematics of Program Construction (1998). http:\/\/www.springerlink.com\/index\/QH44VD66GVE0U3LU.pdf"},{"key":"456_CR9","doi-asserted-by":"crossref","unstructured":"Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: Boehm, BW., Garlan, D., Kramer, J. (eds.) ICSE\u2019 99, pp. 411\u2013420. ACM, Los Angeles, CA, USA (1999)","DOI":"10.1145\/302405.302672"},{"key":"456_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3837-7","volume-title":"A Logical Approach to Discrete Math","author":"D Gries","year":"1993","unstructured":"Gries, D., Schneider, F.B.: A Logical Approach to Discrete Math. Springer, Berlin (1993)"},{"key":"456_CR11","doi-asserted-by":"crossref","unstructured":"Hoang, T., Abrial, J.R.: Reasoning about liveness properties in Event-B. In: Qin, S., Qiu, Z. (eds.) ICFEM, LNCS, vol. 6991, pp. 456\u2013471. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24559-6_31"},{"key":"456_CR12","unstructured":"Hudon, S.: A progress preserving refinement. Master\u2019s thesis. ETH Zurich (2011)"},{"key":"456_CR13","first-page":"57","volume":"280","author":"S Hudon","year":"2011","unstructured":"Hudon, S., Hoang, T.: Development of control systems guided by models of their environment. ENTCS 280, 57\u201368 (2011)","journal-title":"ENTCS"},{"key":"456_CR14","doi-asserted-by":"crossref","unstructured":"Hudon, S., Hoang, T.: Systems design guided by progress concerns. In: Johnsen, EB., Petre, L. (eds.) Proceedings of the 10th International Conference on Integrated Formal Methods (IFM2013), Turku, Finland, June 2013. Integrated Formal Methods. Lecture Notes in Computer Science, vol 7940, pp. 16\u201330. Springer (2013)","DOI":"10.1007\/978-3-642-38613-8_2"},{"key":"456_CR15","unstructured":"Jones, C.B.: Systematic Software Development Using VDM. Prentice Hall International Series in Computer Science. Prentice Hall, Englewood Cliffs (1986)"},{"key":"456_CR16","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125\u2013143 (1977)","DOI":"10.1109\/TSE.1977.229904"},{"issue":"3","key":"456_CR17","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"456_CR18","volume-title":"Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers","author":"L Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Reading (2002)"},{"key":"456_CR19","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Response. In: Manna, Z., Peled, D. (eds.) Time for Verification, Essays in Memory of Amir Pnueli. Lecture Notes in Computer Science, vol. 6200, pp. 279\u2013361. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-13754-9_13"},{"key":"456_CR20","doi-asserted-by":"publisher","unstructured":"Mehta, F.D.: Proofs for the working engineer. Ph.D. thesis, ETH, Zurich (2008). doi: 10.3929\/ethz-a-005635243","DOI":"10.3929\/ethz-a-005635243"},{"key":"456_CR21","doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Poppleton, M.: Formal modelling and verification of population protocols. In: Johnsen, E.B., Petre, L. (eds.) IFM, Lecture Notes in Computer Science, vol. 7940, pp. 208\u2013222. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38613-8_15"},{"key":"456_CR22","unstructured":"Spivey, J.M.: Z Notation\u2014A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edn. Prentice Hall, Englewood Cliffs (1992)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0456-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-015-0456-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0456-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-015-0456-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T11:58:24Z","timestamp":1559131104000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-015-0456-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,15]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["456"],"URL":"https:\/\/doi.org\/10.1007\/s10270-015-0456-2","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,15]]}}}