{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:34:49Z","timestamp":1740123289936,"version":"3.37.3"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"8","license":[{"start":{"date-parts":[[2021,9,7]],"date-time":"2021-09-07T00:00:00Z","timestamp":1630972800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,9,7]],"date-time":"2021-09-07T00:00:00Z","timestamp":1630972800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,12]]},"DOI":"10.1007\/s10817-021-09602-2","type":"journal-article","created":{"date-parts":[[2021,9,7]],"date-time":"2021-09-07T04:02:50Z","timestamp":1630987370000},"page":"1125-1151","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["An Automatically Verified Prototype of the Tokeneer ID Station Specification"],"prefix":"10.1007","volume":"65","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9163-2609","authenticated-orcid":false,"given":"Maximiliano","family":"Cristi\u00e1","sequence":"first","affiliation":[]},{"given":"Gianfranco","family":"Rossi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,9,7]]},"reference":[{"key":"9602_CR1","unstructured":"2011 Microsoft Research Verified Software Milestone Award: Janet Barnes and Rod Chapman for the Tokeneer project, https:\/\/sites.google.com\/site\/verifiedsoftwareinitiative\/mrs-award\/2011-award"},{"key":"9602_CR2","doi-asserted-by":"publisher","unstructured":"Abdelhalim, I., Sharp, J., Schneider, S.A., Treharne, H.: Formal verification of Tokeneer behaviours modelled in fUML using CSP. In: Dong, J.S., Zhu, H. (eds.) Formal Methods and Software Engineering - 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6447, pp. 371\u2013387. Springer (2010), https:\/\/doi.org\/10.1007\/978-3-642-16901-4_25","DOI":"10.1007\/978-3-642-16901-4_25"},{"key":"9602_CR3","unstructured":"Altran UK: Tokeneer software and project documents (2008), http:\/\/www.adacore.com\/uploads\/downloads\/tokeneer.zip"},{"key":"9602_CR4","doi-asserted-by":"crossref","unstructured":"Andr\u00e9ka, H., Givant, S.R., N\u00e9meti, I.: Decision problems for equational theories of relation algebras, vol. 604. American Mathematical Soc. (1997)","DOI":"10.1090\/memo\/0604"},{"key":"9602_CR5","unstructured":"Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., Everett, B.: Engineering the Tokeneer enclave protection software. In: Proceedings of the IEEE International Symposium on Secure Software Engineering. IEEE (2006)"},{"key":"9602_CR6","unstructured":"Barnes, J.: Tokeneer ID Station: Formal specification. Tech. rep., Altran Praxis (2008), http:\/\/www.adacore.com\/uploads\/downloads\/tokeneer.zip, find it as \/tokeneer\/docs\/41\\_2\\_Formal\\_Functional\\_Specification\/41\\_2.pdf inside tokeneer.zip"},{"key":"9602_CR7","unstructured":"Barnes, J.E.: Experiences in the industrial use of formal methods. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 46,(2011)"},{"key":"9602_CR8","doi-asserted-by":"publisher","unstructured":"Betarte, G., Campo, J.D., Luna, C., Romano, A.: Formal analysis of Android\u2019s permission-based security model. Sci. Ann. Comp. Sci. 26(1), 27\u201368 (2016). https:\/\/doi.org\/10.7561\/SACS.2016.1.27","DOI":"10.7561\/SACS.2016.1.27"},{"key":"9602_CR9","unstructured":"Common Criteria Recognition Arrangement: Common criteria for information technology security evaluation, part 1: Introduction and general model, version 3.1. release 5. Tech. rep. (2017), https:\/\/www.commoncriteriaportal.org\/files\/ccfiles\/CCPART1V3.1R5.pdf"},{"key":"9602_CR10","unstructured":"Cooper, D.: Tokeneer ID Station: Security properties. Tech. rep., Altran Praxis (2008), http:\/\/www.adacore.com\/uploads\/downloads\/tokeneer.zip, find it as \/tokeneer\/docs\/40\\_4\\_Security\\_Properties\/40\\_4.pdf inside tokeneer.zip"},{"key":"9602_CR11","unstructured":"Cooper, D., Barnes, J.: Tokeneer ID Station EAL5 demonstrator: Summary report. Tech. rep., Altran Praxis (2008), https:\/\/www.adacore.com\/uploads\/downloads\/Tokeneer_Report.pdf"},{"key":"9602_CR12","unstructured":"Cooper, D., Everett, B., Johnson, R., Widmaier, J.: Security by construction \u2013 Engineering software to exceed EAL5. In: Proceedings of the Fourth Annual High Confidence Software and Systems Conference (2004)"},{"issue":"1","key":"9602_CR13","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1002\/stvr.1477","volume":"24","author":"M Cristi\u00e1","year":"2014","unstructured":"Cristi\u00e1, M., Albertengo, P., Frydman, C.S., Pl\u00fcss, B., Rodr\u00edguez Monetti, P.: Tool support for the test template framework. Softw. Test. Verif. Reliab. 24(1), 3\u201337 (2014)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"9602_CR14","doi-asserted-by":"publisher","unstructured":"Cristi\u00e1, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de\u00a0Moura, L. (ed.) Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10395, pp. 185\u2013201. Springer (2017), https:\/\/doi.org\/10.1007\/978-3-319-63046-5_12","DOI":"10.1007\/978-3-319-63046-5_12"},{"key":"9602_CR15","unstructured":"Cristi\u00e1, M., Rossi, G.: Programming in Java with restricted intensional sets. In: Cristi\u00e1, M., Delahaye, D., Dubois, C. (eds.) Proceedings of the 3rd International Workshop on Sets and Tools co-located with the 6th International ABZ Conference, SETS@ABZ 2018, Southamptom, UK, June 5, 2018. CEUR Workshop Proceedings, vol. 2199, pp. 17\u201331. CEUR-WS.org (2018), http:\/\/ceur-ws.org\/Vol-2199\/paper2.pdf"},{"key":"9602_CR16","doi-asserted-by":"publisher","unstructured":"Cristi\u00e1, M., Rossi, G.: A set solver for finite set relation algebra. In: Desharnais, J., Guttmann, W., Joosten, S. (eds.) Relational and Algebraic Methods in Computer Science - 17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29 - November 1, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11194, pp. 333\u2013349. Springer (2018), https:\/\/doi.org\/10.1007\/978-3-030-02149-8_20","DOI":"10.1007\/978-3-030-02149-8_20"},{"key":"9602_CR17","unstructured":"Cristi\u00e1, M., Rossi, G.: Automated reasoning with restricted intensional sets. CoRR abs\/1910.09118 (2019), http:\/\/arxiv.org\/abs\/1910.09118"},{"issue":"2","key":"9602_CR18","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s10817-019-09520-4","volume":"64","author":"M Cristi\u00e1","year":"2020","unstructured":"Cristi\u00e1, M., Rossi, G.: Solving quantifier-free first-order constraints over finite sets and binary relations. J. Autom. Reason. 64(2), 295\u2013330 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09520-4","journal-title":"J. Autom. Reason."},{"issue":"4","key":"9602_CR19","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/s10817-020-09577-6","volume":"65","author":"M Cristi\u00e1","year":"2021","unstructured":"Cristi\u00e1, M., Rossi, G.: Automated proof of Bell-LaPadula security properties. J. Autom. Reason. 65(4), 463\u2013478 (2021). https:\/\/doi.org\/10.1007\/s10817-020-09577-6","journal-title":"J. Autom. Reason."},{"key":"9602_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09589-w","author":"M Cristi\u00e1","year":"2021","unstructured":"Cristi\u00e1, M., Rossi, G.: Automated reasoning with restricted intensional sets. J. Autom. Reason. (2021). https:\/\/doi.org\/10.1007\/s10817-021-09589-w","journal-title":"J. Autom. Reason."},{"key":"9602_CR21","unstructured":"Cristi\u00e1, M., Rossi, G.: $$\\{log\\}$$: Set formulas as programs. CoRR abs\/2104.08130 (2021), https:\/\/arxiv.org\/abs\/2104.08130"},{"key":"9602_CR22","doi-asserted-by":"crossref","unstructured":"Cristi\u00e1, M., Rossi, G., Frydman, C.S.: log as a test case generator for the Test Template Framework. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM. Lecture Notes in Computer Science, vol. 8137, pp. 229\u2013243. Springer (2013)","DOI":"10.1007\/978-3-642-40561-7_16"},{"issue":"5","key":"9602_CR23","doi-asserted-by":"publisher","first-page":"861","DOI":"10.1145\/365151.365169","volume":"22","author":"A Dovier","year":"2000","unstructured":"Dovier, A., Piazza, C., Pontelli, E., Rossi, G.: Sets and constraint logic programming. ACM Trans. Program. Lang. Syst. 22(5), 861\u2013931 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"9602_CR24","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1017\/S1471068406002730","volume":"6","author":"A Dovier","year":"2006","unstructured":"Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory Pract. Log. Program. 6(6), 645\u2013701 (2006)","journal-title":"Theory Pract. Log. Program."},{"key":"9602_CR25","doi-asserted-by":"publisher","unstructured":"Evans, A.: An improved recipe for specifying reactive systems in Z. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds.) ZUM \u201997: The Z Formal Specification Notation, 10th International Conference of Z Users, Reading, UK, April 3-4, 1997, Proceedings. Lecture Notes in Computer Science, vol. 1212, pp. 275\u2013294. Springer (1997), https:\/\/doi.org\/10.1007\/BFb0027293","DOI":"10.1007\/BFb0027293"},{"key":"9602_CR26","doi-asserted-by":"publisher","unstructured":"Garavel, H., ter Beek, M.H., van\u00a0de Pol, J.: The 2020 expert survey on formal methods. In: ter Beek, M.H., Nickovic, D. (eds.) Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Vienna, Austria, September 2-3, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12327, pp. 3\u201369. Springer (2020), https:\/\/doi.org\/10.1007\/978-3-030-58298-2_1","DOI":"10.1007\/978-3-030-58298-2_1"},{"issue":"1","key":"9602_CR27","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/52.976937","volume":"19","author":"A Hall","year":"2002","unstructured":"Hall, A., Chapman, R.: Correctness by construction: developing a commercial secure system. IEEE Software 19(1), 18\u201325 (2002). https:\/\/doi.org\/10.1109\/52.976937","journal-title":"IEEE Software"},{"key":"9602_CR28","first-page":"209","volume-title":"Lecture notes in computer science","author":"C Holzbaur","year":"1996","unstructured":"Holzbaur, C., Menezes, F., Barahona, P.: Defeasibility in CLP(Q) through generalized slack variables. In: Freuder, E.C. (ed.) Lecture notes in computer science, vol. 1118, pp. 209\u2013223. Springer, Berlin (1996)"},{"key":"9602_CR29","unstructured":"International Electrotechnical Commission: Functional safety of electrical\/electronic\/programmable electronic safety-related systems \u2013 part 1: General requirements. Tech. rep., International Electrotechnical Commission, https:\/\/webstore.iec.ch\/preview\/info_iec61508-1ed2.0b.pdf"},{"key":"9602_CR30","unstructured":"Jackson, P.B., Passmore, G.O.: Proving SPARK verification conditions with SMT solvers. Tech. rep., University of Edinburgh (2009), http:\/\/homepages.inf.ed.ac.uk\/pbj\/papers\/vct-dec09-draft.pdf"},{"key":"9602_CR31","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511574924","volume-title":"The way of Z: practical programming with formal methods","author":"J Jacky","year":"1996","unstructured":"Jacky, J.: The way of Z: practical programming with formal methods. Cambridge University Press, New York, NY, USA (1996)"},{"issue":"8","key":"9602_CR32","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1109\/32.879807","volume":"26","author":"S King","year":"2000","unstructured":"King, S., Hammond, J., Chapman, R., Pryor, A.: Is proof more cost-effective than testing? IEEE Trans. Software Eng. 26(8), 675\u2013686 (2000). https:\/\/doi.org\/10.1109\/32.879807","journal-title":"IEEE Trans. Software Eng."},{"key":"9602_CR33","doi-asserted-by":"publisher","unstructured":"Kuppe, M.A., Lamport, L., Ricketts, D.: The TLA+ toolbox. In: Monahan, R., Prevosto, V., Proen\u00e7a, J. (eds.) Proceedings Fifth Workshop on Formal Integrated Development Environment, F-IDE@FM 2019, Porto, Portugal, 7th October 2019. EPTCS, vol. 310, pp. 50\u201362 (2019), https:\/\/doi.org\/10.4204\/EPTCS.310.6","DOI":"10.4204\/EPTCS.310.6"},{"key":"9602_CR34","doi-asserted-by":"publisher","unstructured":"Lamport, L.: TLZ. In: Bowen, J.P., Hall, J.A. (eds.) Z User Workshop, Cambridge, UK, 29-30 June 1994, Proceedings. pp. 267\u2013268. Workshops in Computing, Springer\/BCS (1994), https:\/\/doi.org\/10.1007\/978-1-4471-3452-7_15","DOI":"10.1007\/978-1-4471-3452-7_15"},{"key":"9602_CR35","unstructured":"Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002), http:\/\/research.microsoft.com\/users\/lamport\/tla\/book.html"},{"issue":"7","key":"9602_CR36","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"9602_CR37","doi-asserted-by":"publisher","DOI":"10.19153\/cleiej.21.2.3","author":"C Luna","year":"2018","unstructured":"Luna, C., Betarte, G., Campo, J.D., Sanz, C., Cristi\u00e1, M., Gorostiaga, F.: A formal approach for the verification of the permission-based security model of Android. CLEI Electron. J. (2018). https:\/\/doi.org\/10.19153\/cleiej.21.2.3","journal-title":"CLEI Electron. J."},{"key":"9602_CR38","unstructured":"Moy, Y., Wallenburg, A.: Tokeneer: Beyond formal program verification. Embed. Real Time Software Syst. 24,(2010)"},{"key":"9602_CR39","doi-asserted-by":"publisher","unstructured":"Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: From general purpose to a proof of information flow enforcement. In: 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013. pp. 415\u2013429. IEEE Computer Society (2013), https:\/\/doi.org\/10.1109\/SP.2013.35","DOI":"10.1109\/SP.2013.35"},{"key":"9602_CR40","doi-asserted-by":"publisher","unstructured":"Nemouchi, Y., Foster, S., Gleirscher, M., Kelly, T.: Isabelle\/SACM: Computer-assisted assurance cases with integrated formal methods. In: Ahrendt, W., Tarifa, S.L.T. (eds.) Integrated Formal Methods - 15th International Conference, IFM 2019, Bergen, Norway, December 2-6, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11918, pp. 379\u2013398. Springer (2019), https:\/\/doi.org\/10.1007\/978-3-030-34968-4_21","DOI":"10.1007\/978-3-030-34968-4_21"},{"key":"9602_CR41","doi-asserted-by":"publisher","unstructured":"Plagge, D., Leuschel, M.: Validating Z specifications using the probanimator and model checker. In: Davies, J., Gibbons, J. (eds.) Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2-5, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4591, pp. 480\u2013500. Springer (2007), https:\/\/doi.org\/10.1007\/978-3-540-73210-5_25","DOI":"10.1007\/978-3-540-73210-5_25"},{"key":"9602_CR42","volume-title":"An introduction to formal specification and Z","author":"B Potter","year":"1996","unstructured":"Potter, B., Sinclair, J., Till, D.: An introduction to formal specification and Z. Prentice Hall PTR Upper Saddle River, NJ, USA (1996)"},{"key":"9602_CR43","doi-asserted-by":"publisher","unstructured":"Rivera, V., Bhattacharya, S., Cata\u00f1o, N.: Undertaking the Tokeneer challenge in Event-B. In: Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2016, Austin, Texas, USA, May 15, 2016. pp. 8\u201314. ACM (2016), https:\/\/doi.org\/10.1145\/2897667.2897671","DOI":"10.1145\/2897667.2897671"},{"key":"9602_CR44","unstructured":"Rossi, G.: $$\\{log\\}$$. http:\/\/people.dmi.unipr.it\/gianfranco.rossi\/setlog.Home.html (2008), last access 2021"},{"issue":"3\u20134","key":"9602_CR45","doi-asserted-by":"publisher","first-page":"393","DOI":"10.3233\/FI-2015-1260","volume":"140","author":"G Rossi","year":"2015","unstructured":"Rossi, G., Bergenti, F.: Nondeterministic programming in Java with JSetL. Fundam. Inform. 140(3\u20134), 393\u2013412 (2015). https:\/\/doi.org\/10.3233\/FI-2015-1260","journal-title":"Fundam. Inform."},{"key":"9602_CR46","doi-asserted-by":"publisher","unstructured":"Schanda, F., Brain, M.: Using answer set programming in the development of verified software. In: Dovier, A., Costa, V.S. (eds.) Technical Communications of the 28th International Conference on Logic Programming, ICLP 2012, September 4-8, 2012, Budapest, Hungary. LIPIcs, vol.\u00a017, pp. 72\u201385. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012), https:\/\/doi.org\/10.4230\/LIPIcs.ICLP.2012.72","DOI":"10.4230\/LIPIcs.ICLP.2012.72"},{"key":"9602_CR47","doi-asserted-by":"publisher","unstructured":"Schwartz, J.T., Dewar, R.B.K., Dubinsky, E., Schonberg, E.: Programming with Sets - An Introduction to SETL. Texts and Monographs in Computer Science, Springer (1986), https:\/\/doi.org\/10.1007\/978-1-4613-9575-1","DOI":"10.1007\/978-1-4613-9575-1"},{"key":"9602_CR48","volume-title":"The Z notation: a reference manual.","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z notation: a reference manual. Prentice Hall International (UK) Ltd., Hertfordshire, UK (1992)"},{"issue":"11","key":"9602_CR49","doi-asserted-by":"publisher","first-page":"777","DOI":"10.1109\/32.553698","volume":"22","author":"P Stocks","year":"1996","unstructured":"Stocks, P., Carrington, D.: A Framework for specification-based testing. IEEE Trans. Software Eng. 22(11), 777\u2013793 (1996)","journal-title":"IEEE Trans. Software Eng."},{"issue":"10","key":"9602_CR50","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1109\/MC.2006.340","volume":"39","author":"J Woodcock","year":"2006","unstructured":"Woodcock, J.: First steps in the verified software grand challenge. Computer 39(10), 57\u201364 (2006). https:\/\/doi.org\/10.1109\/MC.2006.340","journal-title":"Computer"},{"key":"9602_CR51","doi-asserted-by":"crossref","unstructured":"Woodcock, J., Aydal, J., Aydal, E.G., Chapman, R.: The Tokeneer experiments. In: Roscoe, A.W., Jones, C.B., Wood, K.R. (eds.) Reflections on the Work of C. A. R. Hoare, pp. 405\u2013430. Springer (2010)","DOI":"10.1007\/978-1-84882-912-1_17"},{"key":"9602_CR52","unstructured":"Yin, X., Knight, J.C.: Formal verification of large software systems. In: Mu\u00f1oz, C.A. (ed.) Second NASA Formal Methods Symposium - NFM 2010, Washington D.C., USA, April 13-15, 2010. Proceedings. NASA Conference Proceedings, vol. NASA\/CP-2010-216215, pp. 192\u2013201 (2010)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09602-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-021-09602-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-021-09602-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,23]],"date-time":"2021-10-23T05:29:44Z","timestamp":1634966984000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-021-09602-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,7]]},"references-count":52,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["9602"],"URL":"https:\/\/doi.org\/10.1007\/s10817-021-09602-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2021,9,7]]},"assertion":[{"value":"26 January 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 July 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 September 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}