{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T01:36:32Z","timestamp":1742952992710,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030921361"},{"type":"electronic","value":"9783030921378"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-92137-8_5","type":"book-chapter","created":{"date-parts":[[2021,11,30]],"date-time":"2021-11-30T17:38:55Z","timestamp":1638293935000},"page":"70-86","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Temporal Reasoning Through Automatic Translation of\u00a0tock-CSP into\u00a0Timed Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4465-3858","authenticated-orcid":false,"given":"Abdulrazaq","family":"Abba","sequence":"first","affiliation":[]},{"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]},{"given":"Jeremy","family":"Jacob","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,26]]},"reference":[{"key":"5_CR1","unstructured":"A repository of this work. https:\/\/github.com\/ahagmj\/TemporalReasoning.git"},{"key":"5_CR2","unstructured":"Abba, A.: Temporal reasoning about robotics applications: refinement and temporal logic. Ph.D. thesis, The University of York (2021)"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theor. Comput, Sci. 126, 183\u2013235 (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"issue":"1","key":"5_CR4","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/0022-0000(81)90005-2","volume":"23","author":"R Back","year":"1981","unstructured":"Back, R.: On correct refinement of programs. J. Comput. Syst. Sci. 23(1), 49\u201368 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G., H\u00e5kansson, J., Petterson, P., Wang, Y., Hendriks, M.: UPPAAL 4.0. Third Int. Conf. Quant. Eval. Syst. QEST 2006 pp. 125\u2013126 (2006). https:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/j.entcs.2009.02.044","volume":"231","author":"P Bouyer","year":"2009","unstructured":"Bouyer, P.: Model-checking timed temporal logics. Electr. Notes Theor. Comput. Sci. 231, 323\u2013341 (2009)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Bouyer, P.: An introduction to timed automata. In: Seatzu, C., Silva M., van Schuppen J. (eds) Control of Discrete-Event Systems. Lecture Notes in Control and Information Sciences, vol. 433, pp. 79\u201394. Springer, London (2011). https:\/\/doi.org\/10.1007\/978-1-4471-4276-8_9","DOI":"10.1007\/978-1-4471-4276-8_9"},{"issue":"2","key":"5_CR8","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(2), 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"6","key":"5_CR9","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1109\/TSE.2008.52","volume":"34","author":"JS Dong","year":"2008","unstructured":"Dong, J.S., Hao, P., Qin, S., Sun, J., Yi, W.: Timed automata patterns. IEEE Trans. Softw. Eng. 34(6), 844\u2013859 (2008)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11901433_19","volume-title":"Formal Methods and Software Engineering","author":"JS Dong","year":"2006","unstructured":"Dong, J.S., Hao, P., Sun, J., Zhang, X.: A Reasoning method for timed CSP based on constraint solving. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 342\u2013359. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901433_19"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Evans, N., Schneider, S.: Analysing time dependent security properties in CSP using PVS. In: European Symposium on Research in Computer Security. pp. 222\u2013237. Springer (2000)","DOI":"10.1007\/10722599_14"},{"key":"5_CR12","unstructured":"de Freitas, A.F.: From Circus to Java: Implementation and verification of a translation strategy. Master\u2019s thesis, University of York (2005)"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol, Transf. 18, 149\u2013167 (2016)","DOI":"10.1007\/s10009-015-0377-y"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"G\u00f6thel, T., Glesner, S.: Automatic validation of infinite real-time systems. In: 2013 1st FME Workshop on Formal Methods in Software Engineering (FormaliSE), pp. 57\u201363. IEEE (2013)","DOI":"10.1109\/FormaliSE.2013.6612278"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Hansen, D., Leuschel, M.: Translating TLA+ to B for validation with ProB. In: International Conference on Integrated Formal Methods, pp. 24\u201338. Springer (2012)","DOI":"10.1007\/978-3-642-30729-4_3"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Hansen, D., Leuschel, M.: Translating B to TLA+ for validation with TLC. In: International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 40\u201355. Springer (2014)","DOI":"10.1007\/978-3-662-43652-3_4"},{"issue":"8","key":"5_CR17","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Hutton, G.: Programming in Haskell. Cambridge University Press, Cambridge (2016)","DOI":"10.1017\/CBO9781316784099"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-30729-4_5","volume-title":"Integrated Formal Methods","author":"Y Isobe","year":"2012","unstructured":"Isobe, Y., Moller, F., Nguyen, H.N., Roggenbach, M.: Safety and line capacity in railways \u2013 an approach in timed CSP. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 54\u201368. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30729-4_5"},{"issue":"4","key":"5_CR20","doi-asserted-by":"publisher","first-page":"2361","DOI":"10.1007\/s10270-018-0665-6","volume":"18","author":"N Kahani","year":"2018","unstructured":"Kahani, N., Bagherzadeh, M., Cordy, J.R., Dingel, J., Varr\u00f3, D.: Survey and classification of model transformation tools. Softw. Syst. Model. 18(4), 2361\u20132397 (2018). https:\/\/doi.org\/10.1007\/s10270-018-0665-6","journal-title":"Softw. Syst. Model."},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Khattri, M.: Translating timed automata to tock-CSP. In: Proceedings of the 10th IASTED International Conference on Software Engineering, SE 2011 (2011)","DOI":"10.2316\/P.2011.720-047"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Lindstrom, B., Pettersson, P., Offutt, J.: Generating trace-sets for model-based testing. In: The 18th IEEE International Symposium on Software Reliability (ISSRE\u201907), pp. 171\u2013180. IEEE (2007)","DOI":"10.1109\/ISSRE.2007.15"},{"issue":"3","key":"5_CR23","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s00165-007-0065-0","volume":"20","author":"G Lowe","year":"2008","unstructured":"Lowe, G.: Specification of communicating processes: temporal logic versus refusals-based refinement. Form Aspect. Comput. 20(3), 277\u2013294 (2008)","journal-title":"Form Aspect. Comput."},{"key":"5_CR24","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.entcs.2005.10.021","volume":"152","author":"T Mens","year":"2006","unstructured":"Mens, T., Van Gorp, P.: A taxonomy of model transformation. Electr. Rotes Theoret. Comput. Sci. 152, 125\u2013142 (2006)","journal-title":"Electr. Rotes Theoret. Comput. Sci."},{"key":"5_CR25","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J., Woodcock, J.: RoboChart: a State-Machine Notation for Modelling and Verification of Mobile and Autonomous Robots. Tech. Rep. pp. 1\u201318 (2016)"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Nielson, H.R., Nielson, F.: Semantics with Applications: an Appetizer. Springer Science & Business Media, London (2007)","DOI":"10.1007\/978-1-84628-692-6"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Nogueira, S., Sampaio, A., Mota, A.: Guided test generation from CSP models. In: International Colloquium on Theoretical Aspects of Computing. pp. 258\u2013273. Springer, Cham (2008). https:\/\/doi.org\/10.1007\/978-3-030-85315-0","DOI":"10.1007\/978-3-030-85315-0"},{"key":"5_CR28","unstructured":"Oliveira, M.V.M.: Formal derivation of state-rich reactive programs using Circus. Ph.D. thesis, University of York (2005)"},{"key":"5_CR29","unstructured":"Ouaknine, J.: Discrete analysis of continuous behaviour in real-time concurrent systems. Ph.D. thesis, University of Oxford (2000)"},{"issue":"2","key":"5_CR30","first-page":"99","volume":"10","author":"J Ouaknine","year":"2003","unstructured":"Ouaknine, J., Worrell, J.: Timed-CSP = closed timed $$\\varepsilon $$-automata. Nordic J. Comput. 10(2), 99\u2013133 (2003)","journal-title":"Nordic J. Comput."},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Springer Science & Business Media, London (2010)","DOI":"10.1007\/978-1-84882-258-0"},{"key":"5_CR32","unstructured":"Roscoe, A., Hoare, C., Bird, R.: The theory and practice of concurrency. 2005. Revised edition. Only available online (2005)"},{"key":"5_CR33","unstructured":"Schneider, S.: Concurrent and real time systems: the CSP approach. In: World Scientific Proceedings Series on Computer Engineering and Information Science (2010)"},{"key":"5_CR34","doi-asserted-by":"publisher","unstructured":"Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., Andr\u00e9, E.: Modeling and verifying hierarchical real-time systems using stateful Timed-CSP. ACM Trans. Softw. Eng. Methodol. 22(1) (2013). https:\/\/doi.org\/10.1145\/2430536.2430537, https:\/\/doi.org\/10.1145\/2430536.2430537","DOI":"10.1145\/2430536.2430537"},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709\u2013714. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_59"},{"issue":"1","key":"5_CR36","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10009-015-0402-1","volume":"19","author":"K Ye","year":"2017","unstructured":"Ye, K., Woodcock, J.: Model checking of state-rich formalism by linking to $$CSP \\parallel B$$. Int. J. Softw. Tools Technol. Transf. 19(1), 73\u201396 (2017)","journal-title":"Int. J. Softw. Tools Technol. Transf."}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-92137-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,4]],"date-time":"2021-12-04T00:06:25Z","timestamp":1638576385000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-92137-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030921361","9783030921378"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-92137-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"26 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SBMF","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazilian Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 December 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sbmf2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sites.google.com\/computacao.ufcg.edu.br\/sbmf2021\/home","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}