{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:04:23Z","timestamp":1742911463836,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319671123"},{"type":"electronic","value":"9783319671130"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-67113-0_2","type":"book-chapter","created":{"date-parts":[[2017,8,24]],"date-time":"2017-08-24T00:21:24Z","timestamp":1503534084000},"page":"19-33","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Event-Based Timing Constraints by Translation into Presburger Formulae"],"prefix":"10.1007","author":[{"given":"Bj\u00f6rn","family":"Lisper","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,25]]},"reference":[{"issue":"5","key":"2_CR1","doi-asserted-by":"crossref","first-page":"1543","DOI":"10.1145\/186025.186058","volume":"16","author":"M Abadi","year":"1994","unstructured":"Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Trans. Program. Lang. Syst. 16(5), 1543\u20131571 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceeding of Logic in Computer Science, pp. 414\u2013425. IEEE (1990)","DOI":"10.1109\/LICS.1990.113766"},{"issue":"1","key":"2_CR3","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","volume":"41","author":"R Alur","year":"1994","unstructured":"Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181\u2013203 (1994)","journal-title":"J. ACM"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Amon, T., Borriello, G., Hu, T., Liu, J.: Symbolic timing verification of timing diagrams using Presburger formulas. In: Proceeding of 34th Annual Design Automation Conference, pp. 226\u2013231. ACM, New York (1997)","DOI":"10.1109\/DAC.1997.597148"},{"key":"2_CR5","unstructured":"Andr\u00e9, C., Mallet, F.: Clock constraints in UML\/MARTE CCSL. Research report, INRIA, May 2008"},{"key":"2_CR6","unstructured":"AUTOSAR: Homepage of the AUTOSAR project (2009). www.autosar.org\/"},{"key":"2_CR7","unstructured":"AUTOSAR: Specification of timing extensions (2011). www.autosar.org\/"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Baruah, S., Buttazzo, G., Gorinsky, S., Lipari, G.: Scheduling periodic task systems to minimize output jitter. In: Proceeding of Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA 1999), pp. 62\u201369 (1999)","DOI":"10.1109\/RTCSA.1999.811194"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-319-45943-1_13","volume-title":"Critical Systems: Formal Methods and Automated Verification","author":"S Beringer","year":"2016","unstructured":"Beringer, S., Wehrheim, H.: Verification of AUTOSAR software architectures with timed automata. In: Beek, M.H., Gnesi, S., Knapp, A. (eds.) FMICS\/AVoCS 2016. LNCS, vol. 9933, pp. 189\u2013204. Springer, Cham (2016). doi: 10.1007\/978-3-319-45943-1_13"},{"key":"2_CR10","unstructured":"Blom, H., Feng, L., L\u00f6nn, H., Nordlander, J., Kuntz, S., Lisper, B., Quinton, S., Hanke, M., Peraldi-Frati, M.A., Goknil, A., Deantoni, J., Defo, G.B., Klobedanz, K., \u00d6zhan, M., Honcharova, O.: D11 language syntax, semantics, metamodel v2. Technical report, August 2012. https:\/\/itea3.org\/project\/timmo-2-use.html"},{"issue":"5","key":"2_CR11","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z Chaochen","year":"1991","unstructured":"Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269\u2013276 (1991)","journal-title":"Inf. Process. Lett."},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-642-16277-0_11","volume-title":"Model-Based Engineering of Embedded Real-Time Systems","author":"P Cuenot","year":"2010","unstructured":"Cuenot, P., et al.: 11 The EAST-ADL architecture description language for automotive embedded software. In: Giese, H., Karsai, G., Lee, E., Rumpe, B., Sch\u00e4tz, B. (eds.) MBEERTS 2007. LNCS, vol. 6100, pp. 297\u2013307. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-16277-0_11"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/978-3-642-31491-9_27","volume-title":"Modelling Foundations and Applications","author":"N Ge","year":"2012","unstructured":"Ge, N., Pantel, M.: Time properties verification framework for UML-MARTE safety critical real-time systems. In: Vallecillo, A., Tolvanen, J.-P., Kindler, E., St\u00f6rrle, H., Kolovos, D. (eds.) ECMFA 2012. LNCS, vol. 7349, pp. 352\u2013367. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31491-9_27"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52\u201353, 183\u2013220 (2002). http:\/\/dx.doi.org\/10.1016\/S1567-8326(02)00037-1","DOI":"10.1016\/S1567-8326(02)00037-1"},{"key":"2_CR15","unstructured":"Johansson, R., Frey, P., Jonsson, J., Nordlander, J., Pathan, R.M., Feiertag, N., Schlager, M., Espinoza, H., Richter, K., Kuntz, S., L\u00f6nn, H., Kolagari, R.T., Blom, H.: TADL: timing augmented description language, version 2. Technical report, October 2009"},{"key":"2_CR16","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1, 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-642-34032-1_12","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies","author":"B Lisper","year":"2012","unstructured":"Lisper, B., Nordlander, J.: A simple and flexible timing constraint logic. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7610, pp. 80\u201395. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-34032-1_12"},{"issue":"1","key":"2_CR18","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1145\/321738.321743","volume":"20","author":"C Liu","year":"1973","unstructured":"Liu, C., Layland, J.: Scheduling algorithms for multiprogramming in a hard-real-time environment. J. ACM 20(1), 46\u201361 (1973)","journal-title":"J. ACM"},{"key":"2_CR19","unstructured":"Mok, A.K.: Fundamental design problems of distributed systems for the hard-real-time environment. Ph.D. thesis, Massachusetts Institute of Technology, May 1983"},{"key":"2_CR20","unstructured":"UML profile for MARTE: modeling and analysis of real-time embedded systems. Technical report, OMG, November 2009"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Suryadevara, J.: Validating EAST-ADL timing constraints using UPPAAL. In: Proceeding 39th Euromicro Conference on Software Engineering and Advanced Applications (SEAA), September 2013. http:\/\/www.es.mdh.se\/publications\/2988-22","DOI":"10.1109\/SEAA.2013.46"},{"key":"2_CR22","unstructured":"Verdoolaege, S.: barvinok: user guide. Technical report, January 2016. barvinok.gforge.inria.fr\/barvinok.pdf"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Yin, L., Mallet, F., Liu, J.: Verification of MARTE\/CCSL time requirements in Promela\/SPIN. In: Proceeding of 16th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2011), pp. 65\u201374, April 2011","DOI":"10.1109\/ICECCS.2011.14"}],"container-title":["Lecture Notes in Computer Science","Critical Systems: Formal Methods and Automated Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67113-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T14:48:51Z","timestamp":1570027731000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67113-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319671123","9783319671130"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67113-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}