{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T14:29:14Z","timestamp":1784644154817,"version":"3.55.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030317836","type":"print"},{"value":"9783030317843","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-31784-3_7","type":"book-chapter","created":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T21:32:04Z","timestamp":1571607124000},"page":"115-130","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Parametric Timed Model Checking for Guaranteeing Timed Opacity"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8473-9555","authenticated-orcid":false,"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3545-1392","authenticated-orcid":false,"given":"Jun","family":"Sun","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,10,21]]},"reference":[{"key":"7_CR1","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-319-53946-1_5","volume-title":"Formal Techniques for Safety-Critical Systems","author":"IH Abbasi","year":"2017","unstructured":"Abbasi, I.H., Lodhi, F.K., Kamboh, A.M., Hasan, O.: Formal verification of gate-level multiple side channel parameters to detect hardware Trojans. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2016. CCIS, vol. 694, pp. 75\u201392. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-53946-1_5"},{"issue":"2","key":"7_CR2","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. TCS 126(2), 183\u2013235 (1994). \nhttps:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"TCS"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Kosaraju, S.R., Johnson, D.S., Aggarwal, A. (eds.) STOC, pp. 592\u2013601. ACM, New York (1993). \nhttps:\/\/doi.org\/10.1145\/167088.167242","DOI":"10.1145\/167088.167242"},{"issue":"2","key":"7_CR4","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s10009-017-0467-0","volume":"21","author":"\u00c9 Andr\u00e9","year":"2019","unstructured":"Andr\u00e9, \u00c9.: What\u2019s decidable about parametric timed automata? STTT 21(2), 203\u2013219 (2019). \nhttps:\/\/doi.org\/10.1007\/s10009-017-0467-0","journal-title":"STTT"},{"issue":"5","key":"7_CR5","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1142\/S0129054109006905","volume":"20","author":"\u00c9 Andr\u00e9","year":"2009","unstructured":"Andr\u00e9, \u00c9., Chatain, T., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. IJFCS 20(5), 819\u2013836 (2009). \nhttps:\/\/doi.org\/10.1142\/S0129054109006905","journal-title":"IJFCS"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-642-32759-9_6","volume-title":"FM 2012: Formal Methods","author":"\u00c9 Andr\u00e9","year":"2012","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., K\u00fchne, U., Soulat, R.: IMITATOR 2.5: a tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 33\u201336. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32759-9_6"},{"issue":"1\u20132","key":"7_CR7","first-page":"1","volume":"51","author":"R Barbuti","year":"2002","unstructured":"Barbuti, R., Francesco, N.D., Santone, A., Tesei, L.: A notion of non-interference for timed automata. FI 51(1\u20132), 1\u201311 (2002)","journal-title":"FI"},{"issue":"2","key":"7_CR8","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1080\/00207179.2014.944356","volume":"88","author":"G Benattar","year":"2015","unstructured":"Benattar, G., Cassez, F., Lime, D., Roux, O.H.: Control and synthesis of non-interferent timed systems. Int. J. Control 88(2), 217\u2013236 (2015). \nhttps:\/\/doi.org\/10.1080\/00207179.2014.944356","journal-title":"Int. J. Control"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-02617-1_3","volume-title":"Advances in Information Security and Assurance","author":"F Cassez","year":"2009","unstructured":"Cassez, F.: The dark side of timed opacity. In: Park, J.H., Chen, H.-H., Atiquzzaman, M., Lee, C., Kim, T., Yeo, S.-S. (eds.) ISA 2009. LNCS, vol. 5576, pp. 21\u201330. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02617-1_3"},{"key":"7_CR10","doi-asserted-by":"publisher","unstructured":"Chattopadhyay, S., Roychoudhury, A.: Scalable and precise refinement of cache timing analysis via model checking. In: RTSS, pp. 193\u2013203 (2011). \nhttps:\/\/doi.org\/10.1109\/RTSS.2011.25","DOI":"10.1109\/RTSS.2011.25"},{"key":"7_CR11","doi-asserted-by":"publisher","unstructured":"Chu, D., Jaffar, J., Maghareh, R.: Precise cache timing analysis via symbolic execution. In: RTAS, pp. 293\u2013304 (2016). \nhttps:\/\/doi.org\/10.1109\/RTAS.2016.7461358","DOI":"10.1109\/RTAS.2016.7461358"},{"key":"7_CR12","unstructured":"Doychev, G., Feld, D., K\u00f6pf, B., Mauborgne, L., Reineke, J.: Cacheaudit: a tool for the static analysis of cache side channels. In: King, S.T. (ed.) USENIX Security Symposium, pp. 431\u2013446. USENIX Association (2013)"},{"issue":"1","key":"7_CR13","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.entcs.2005.05.046","volume":"180","author":"G Gardey","year":"2007","unstructured":"Gardey, G., Mullins, J., Roux, O.H.: Non-interference control synthesis for security timed automata. ENTCS 180(1), 35\u201353 (2007). \nhttps:\/\/doi.org\/10.1016\/j.entcs.2005.05.046","journal-title":"ENTCS"},{"key":"7_CR14","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/S1567-8326(02)00037-1","volume":"52\u201353","author":"T Hune","year":"2002","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. JLAP 52\u201353, 183\u2013220 (2002). \nhttps:\/\/doi.org\/10.1016\/S1567-8326(02)00037-1","journal-title":"JLAP"},{"issue":"5","key":"7_CR15","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1109\/TSE.2014.2357445","volume":"41","author":"A Jovanovi\u0107","year":"2015","unstructured":"Jovanovi\u0107, A., Lime, D., Roux, O.H.: Integer parameter synthesis for real-time systems. TSE 41(5), 445\u2013461 (2015). \nhttps:\/\/doi.org\/10.1109\/TSE.2014.2357445","journal-title":"TSE"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/3-540-68697-5_9","volume-title":"Advances in Cryptology \u2014 CRYPTO \u201996","author":"PC Kocher","year":"1996","unstructured":"Kocher, P.C.: Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol. 1109, pp. 104\u2013113. Springer, Heidelberg (1996). \nhttps:\/\/doi.org\/10.1007\/3-540-68697-5_9"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Lv, M., Yi, W., Guan, N., Yu, G.: Combining abstract interpretation with model checking for timing analysis of multicore software. In: RTSS, pp. 339\u2013349. IEEE Computer Society (2010). \nhttps:\/\/doi.org\/10.1109\/RTSS.2010.30","DOI":"10.1109\/RTSS.2010.30"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63121-9_1","volume-title":"Models, Algorithms, Logics and Tools","author":"F Nielson","year":"2017","unstructured":"Nielson, F., Nielson, H.R., Vasilikos, P.: Information flow for timed automata. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 3\u201321. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63121-9_1"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-319-89722-6_2","volume-title":"Principles of Security and Trust","author":"P Vasilikos","year":"2018","unstructured":"Vasilikos, P., Nielson, F., Nielson, H.R.: Secure information release in timed automata. In: Bauer, L., K\u00fcsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 28\u201352. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-89722-6_2"},{"issue":"2","key":"7_CR20","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/3090064.3090071","volume":"4","author":"C Wang","year":"2017","unstructured":"Wang, C., Schaumont, P.: Security by compilation: an automated approach to comprehensive side-channel resistance. SIGLOG News 4(2), 76\u201389 (2017). \nhttps:\/\/doi.org\/10.1145\/3090064.3090071","journal-title":"SIGLOG News"},{"key":"7_CR21","doi-asserted-by":"publisher","unstructured":"Wu, M., Guo, S., Schaumont, P., Wang, C.: Eliminating timing side-channel leaks using program repair. In: Tip, F., Bodden, E. (eds.) ISSTA, pp. 15\u201326. ACM (2018). \nhttps:\/\/doi.org\/10.1145\/3213846.3213851","DOI":"10.1145\/3213846.3213851"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-319-96142-2_12","volume-title":"Computer Aided Verification","author":"J Zhang","year":"2018","unstructured":"Zhang, J., Gao, P., Song, F., Wang, C.: SCInfer: refinement-based verification of software countermeasures against side-channel attacks. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 157\u2013177. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-96142-2_12"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-31784-3_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,14]],"date-time":"2019-11-14T13:28:54Z","timestamp":1573738134000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-31784-3_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030317836","9783030317843"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-31784-3_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"21 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taipei","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taiwan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva2019.iis.sinica.edu.tw\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","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":"87","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":"29","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":"33% - 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.4","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":"Between 1 and 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)"}}]}}