{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T23:07:08Z","timestamp":1764284828875,"version":"3.46.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032120854"},{"type":"electronic","value":"9783032120861"}],"license":[{"start":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T00:00:00Z","timestamp":1764201600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T00:00:00Z","timestamp":1764201600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-12086-1_2","type":"book-chapter","created":{"date-parts":[[2025,11,26]],"date-time":"2025-11-26T08:36:10Z","timestamp":1764146170000},"page":"19-36","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Modular Orthogonal Integration of\u00a0Operational and\u00a0Prescriptive Timing Requirements Using TASTD"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-1996-2434","authenticated-orcid":false,"given":"Alex Rodrigue","family":"Ndouna","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4402-2514","authenticated-orcid":false,"given":"Marc","family":"Frappier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9088-9821","authenticated-orcid":false,"given":"Fr\u00e9d\u00e9ric","family":"Mallet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,27]]},"reference":[{"issue":"2","key":"2_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"key":"2_CR2","unstructured":"Andr\u00e9, C.: Syntax and Semantics of the Clock Constraint Specification Language (CCSL). Research Report RR-6925, INRIA (2009). https:\/\/inria.hal.science\/inria-00384077"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"de\u00a0Azevedo\u00a0Oliveira, D., Frappier, M.: TASTD: A real-time extension for ASTD. In: Gl\u00e4sser, U., Campos, J.C., M\u00e9ry, D., Palanque, P.A. (eds.) ABZ 2023. LNCS, vol. 14010, pp. 142\u2013159. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-33163-3_11","DOI":"10.1007\/978-3-031-33163-3_11"},{"key":"2_CR4","unstructured":"de\u00a0Azevedo\u00a0Oliveira, D., Frappier, M.: Technical Report 27 - Extending ASTD with real-time. https:\/\/github.com\/DiegoOliveiraUDES\/astd-tech-report-27 (2023)"},{"issue":"2","key":"2_CR5","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1002\/SPE.1006","volume":"41","author":"G Behrmann","year":"2011","unstructured":"Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing UPPAAL over 15 years. Softw. Pract. Exp. 41(2), 133\u2013142 (2011). https:\/\/doi.org\/10.1002\/SPE.1006","journal-title":"Softw. Pract. Exp."},{"issue":"1","key":"2_CR6","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1109\/JPROC.2002.805826","volume":"91","author":"A Benveniste","year":"2003","unstructured":"Benveniste, A., Caspi, P., Edwards, S.A., Halbwachs, N., Le Guernic, P., de Simone, R.: The synchronous languages 12 years later. Proc. IEEE 91(1), 64\u201383 (2003)","journal-title":"Proc. IEEE"},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Cartellier, Q., Frappier, M., Mammar, A.: Proving local invariants in ASTDs. In: Li, Y., Tahar, S. (eds.) ICFEM 2023. Lecture Notes in Computer Science, vol. 14308, pp. 228\u2013246. Springer (2023). https:\/\/doi.org\/10.1007\/978-981-99-7584-6_14","DOI":"10.1007\/978-981-99-7584-6_14"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: The nuxmv symbolic model checker. In: CAV 2014. LNCS, vol.\u00a08559, pp. 334\u2013342. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Chen, C., Rivi\u00e8re, P., Singh, N.K., Dupont, G., Ait\u00a0Ameur, Y., Frappier, M.: A proof-based ground algebraic meta-model for reasoning on astd in event-b. In: O\u2019Conner, L. (ed.) IEEE\/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE) (2025)","DOI":"10.1109\/FormaliSE66629.2025.00011"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Chen, X., Mallet, F., Liu, X.: Formally verifying sequence diagrams for safety critical systems. In: Aoki, T., Li, Q. (eds.) TASE 2020, pp. 217\u2013224. IEEE (Dec 2020). https:\/\/doi.org\/10.1109\/TASE49443.2020.00037","DOI":"10.1109\/TASE49443.2020.00037"},{"issue":"5","key":"2_CR11","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1016\/S0022-0000(71)80013-2","volume":"5","author":"F Commoner","year":"1971","unstructured":"Commoner, F., Holt, A.W., Even, S., Pnueli, A.: Marked directed graphs. J. Comput. Syst. Sci. 5(5), 511\u2013523 (1971)","journal-title":"J. Comput. Syst. Sci."},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"DeAntoni, J., Mallet, F.: TimeSquare: treat your models with logical time. In: Furia, C.A., Nanz, S. (eds.) TOOLS 2012. LNCS, vol. 7304, pp. 34\u201341. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30561-0_4","DOI":"10.1007\/978-3-642-30561-0_4"},{"key":"2_CR13","unstructured":"Frappier, M.: ASTD support tools repo. https:\/\/github.com\/DiegoOliveiraUDES\/ASTD-tools (2023)"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"2_CR15","unstructured":"Mallet, F.: LightCCSL tools repo. https:\/\/github.com\/frederic-mallet\/ccsl-sts"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Mallet, F.: Automatic generation of observers from MARTE\/CCSL. In: RSP 2012, pp. 86\u201392. IEEE (2012).https:\/\/doi.org\/10.1109\/RSP.2012.6380695","DOI":"10.1109\/RSP.2012.6380695"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Mallet, F., Millo, J.V.: Boundness issues in CCSL specifications. In: ICFEM 2013 . LNCS, vol.\u00a08144, pp. 20\u201335. Springer (Oct 2013). https:\/\/doi.org\/10.1007\/978-3-642-41202-8_3","DOI":"10.1007\/978-3-642-41202-8_3"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Mallet, F., de\u00a0Simone, R.: Correctness issues on marte\/ccsl constraints. Sci. Comput. Program. 106(C), 78\u201392 (Aug 2015). https:\/\/doi.org\/10.1016\/j.scico.2015.03.001","DOI":"10.1016\/j.scico.2015.03.001"},{"key":"2_CR19","unstructured":"Mallet, F., Millo, J.V., de\u00a0Simone, R.: Safe ccsl specifications and marked graphs. In: (MEMOCODE 2013), pp. 157\u2013166 (2013)"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"2_CR21","unstructured":"Ndouna, A.R., Frappier, M.: Case Study TCS ASTD. https:\/\/github.com\/ndounalex\/CCSL-to-ASTD-translation (2024)"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Nganyewou Tidjon, L., Frappier, M., Leuschel, M., Mammar, A.: Extended algebraic state-transition diagrams. In: 2018 23rd International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 146\u2013155. Melbourne, Australia (2018)","DOI":"10.1109\/ICECCS2018.2018.00023"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Peraldi-Frati, M., DeAntoni, J.: Scheduling multi clock real time systems: from requirements to implementation. In: 14th IEEE ISORC 2011, pp. 50\u201357. IEEE CS (2011). https:\/\/doi.org\/10.1109\/ISORC.2011.16","DOI":"10.1109\/ISORC.2011.16"},{"issue":"2","key":"2_CR24","doi-asserted-by":"publisher","first-page":"835","DOI":"10.1109\/TR.2022.3219649","volume":"73","author":"P Rivi\u00e8re","year":"2024","unstructured":"Rivi\u00e8re, P., Singh, N.K., A\u00eft-Ameur, Y.: Reflexive event-b: Semantics and correctness the EB4EB framework. IEEE Trans. Reliab. 73(2), 835\u2013850 (2024). https:\/\/doi.org\/10.1109\/TR.2022.3219649","journal-title":"IEEE Trans. Reliab."},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"Sp\u00f6nemann, M., Schulze, C.D., Motika, C., Schneider, C., von Hanxleden, R.: KIELER: building on automatic layout for pragmatics-aware modeling. In: Kelleher, C., Burnett, M.M., Sauer, S. (eds.) 2013 IEEE VL\/HCC, pp. 195\u2013196. IEEE Computer Society (2013). https:\/\/doi.org\/10.1109\/VLHCC.2013.6645265","DOI":"10.1109\/VLHCC.2013.6645265"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., Andr\u00e9, \u00c9.: Modeling and verifying hierarchical real-time systems using stateful timed CSP. ACM Trans. Softw. Eng. Methodol. 22(1), 3:1\u20133:29 (2013). https:\/\/doi.org\/10.1145\/2430536.2430537","DOI":"10.1145\/2430536.2430537"},{"key":"2_CR27","first-page":"1","volume-title":"Software Engineering and Formal Methods","author":"J Suryadevara","year":"2013","unstructured":"Suryadevara, J., Seceleanu, C., Mallet, F., Pettersson, P.: Verifying marte\/ccsl mode behaviors using uppaal. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) Software Engineering and Formal Methods, pp. 1\u201315. Springer, Berlin Heidelberg, Berlin, Heidelberg (2013)"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Winskel, G.: Event structures. In: Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course. LNCS, vol.\u00a0255, pp. 325\u2013392. Springer (1986). https:\/\/doi.org\/10.1007\/3-540-17906-2_31","DOI":"10.1007\/3-540-17906-2_31"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-030-16722-6_4","volume-title":"Fundamental Approaches to Software Engineering","author":"M Zhang","year":"2019","unstructured":"Zhang, M., Song, F., Mallet, F., Chen, X.: SMT-based bounded schedulability analysis of the clock constraint specification language. In: H\u00e4hnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 61\u201378. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-16722-6_4"}],"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-032-12086-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,27]],"date-time":"2025-11-27T23:02:08Z","timestamp":1764284528000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-12086-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,27]]},"ISBN":["9783032120854","9783032120861"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-12086-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,11,27]]},"assertion":[{"value":"27 November 2025","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":"Recife","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 December 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sbmf2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sbmf2025.ufrpe.br\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}