{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:43Z","timestamp":1761611323544,"version":"3.40.4"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2014,5,1]],"date-time":"2014-05-01T00:00:00Z","timestamp":1398902400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The design of a complex embedded control system involves integration of large number of components. These components need to interact in a timely fashion to achieve the system level end-to-end requirements. In practice, the component level timing specification consists of design attributes like component task mapping, task period and schedule definition but often lack details on their real-time (functional) requirements. As we observe, there is no systematic methodology in place for decomposing the feature level timing requirements into component level timing requirements. This paper proposes an early stage<jats:italic>time-budgeting methodology<\/jats:italic>to bridge the above gap. A salient proposal of this methodology is to consider<jats:italic>parameterized<\/jats:italic>component timing-requirements. A key step in the methodology involves computing a set of constraints by relating component requirements with feature requirements. This enables the separation of timing constraints from functionality decomposition, and facilitates early optimization of the<jats:italic>component time-budget<\/jats:italic>for a complex component based embedded system. This paper formalizes the proposed methodology by using Parametric Temporal Logic. A case study involving two advanced features from the automotive domain, namely Adaptive Cruise Control and Collision Mitigation is given to demonstrate the methodology.<\/jats:p>","DOI":"10.1007\/s00165-012-0273-0","type":"journal-article","created":{"date-parts":[[2013,3,26]],"date-time":"2013-03-26T14:08:39Z","timestamp":1364306919000},"page":"591-621","source":"Crossref","is-referenced-by-count":5,"title":["<i>Time-budgeting<\/i>: a component based development methodology for real-time embedded systems"],"prefix":"10.1145","volume":"26","author":[{"given":"Manoj G.","family":"Dixit","sequence":"first","affiliation":[{"name":"India Science Lab, General Motors Global Research and Development, Bangalore, India"}]},{"given":"S.","family":"Ramesh","sequence":"additional","affiliation":[{"name":"India Science Lab, General Motors Global Research and Development, Bangalore, India"}]},{"given":"Pallab","family":"Dasgupta","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology, Kharagpur, India"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/377978.377990"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1025"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Alur R Henzinger TA Vardi MY (1993) Parametric real-time reasoning. In: Annual ACM symposium on theory of computing pp 592\u2013601","DOI":"10.1145\/167088.167242"},{"key":"e_1_2_1_2_5_2","unstructured":"ATESST (2008) EAST-ADL 2.0 Specification 2nd edn. http:\/\/www.atesst.org\/home\/liblocal\/docs\/EAST-ADL-2.0-Specification_2008-02-29.pdf"},{"key":"e_1_2_1_2_6_2","unstructured":"AUTOSAR (2010) Methodology 4th edn. http:\/\/www.autosar.org\/download\/R4.0\/AUTOSAR_TR_Methodology.pdf"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Buckl C Goponova I Geisinger M Knoll A Lee EA (2010) Model-based specification of timing requirements. In: International conference on embedded software pp 239\u2013248","DOI":"10.1145\/1879021.1879053"},{"key":"e_1_2_1_2_8_2","unstructured":"Blom H Johansson R Lonn H (2009) Annotation with timing constraints in the context of EAST-ADL2 and AUTOSAR\u2014the Timing Augmented Description Language. In: Workshop on the definition evaluation and exploitation of modelling and computing standards for real-time embedded systems"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bartolini C Lipari G Di Natale M (2005) From functional blocks to the synthesis of the architectural model in embedded real-time applications. In: IEEE real time and embedded technology and applications symposium pp 458\u2013467","DOI":"10.1109\/RTAS.2005.24"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Cimatti A Clarke E Giunchiglia E Giunchiglia F Pistore M Roveri M Sebastiani R Tacchella A (2002) NuSMV 2: an open source tool for symbolic model checking. In: Proceedings of international conference on computer-aided verification pp 241\u2013268","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Clarke EM Emerson EA Sistla AP (1983) Automatic verification of finite-state concurrent system using temporal logic specifications: a practical approach. In: 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages pp 117\u2013126","DOI":"10.1145\/567067.567080"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.5555\/332656"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Dwyer MB Avrunin GS Corbett JC (1999) Patterns in property specifications for finite-state verification. In: International conference on software engineering pp 411\u2013420","DOI":"10.1145\/302405.302672"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Dixit MG Dasgupta P Ramesh S (2010) Taming the component timing: a CBD methodology for real-time embedded systems. In: Design automation and test in europe pp 1649\u20131652","DOI":"10.1109\/DATE.2010.5457077"},{"key":"e_1_2_1_2_15_2","unstructured":"Dutertre B De Moura L (2006) The Yices SMT Solver. Technical report http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Damm W Metzner A (2007) A design methodology for distributed real-time automotive applications. In: GM R&D workshop on next generation design and verification methodologies for distributed embedded systems pp 157\u2013174","DOI":"10.1007\/978-1-4020-6254-4_13"},{"key":"e_1_2_1_2_17_2","unstructured":"Dixit MG Ramesh S Dasgupta P (2010) A case study to demonstrate effectiveness of time-budgeting methodology. Technical report http:\/\/www.facweb.iitkgp.ernet.in\/~pallab\/TimeBudgeting-Case-Study-RTS.pdf"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2011.07.002"},{"key":"e_1_2_1_2_19_2","unstructured":"Damm W Votintseva A Metzner A Josko B Peikenkamp T Bode E (2005) Boosting re-use of embedded automotive applications through rich components. In: Foundations of interface technologies"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Davare A Zhu Q Di Natale M Pinello C Kanajan S Sangiovanni-Vincentelli AL (2007) Period optimization for hard real-time distributed automotive systems. In: Design and automation conference pp 278\u2013283","DOI":"10.1109\/DAC.2007.375172"},{"key":"e_1_2_1_2_21_2","unstructured":"2011. http:\/\/www.eclipse.org."},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Emerson EA Mok AK Sistla AP Srinivasan J (1990) Quantitative temporal reasoning. In: Computer aided verification pp 136\u2013145","DOI":"10.1007\/BFb0023727"},{"key":"e_1_2_1_2_23_2","unstructured":"Emerson EA Trefler RJ (1999) Parametric quantitative temporal reasoning. In: IEEE symposiam on logic in computer science pp 336\u2013343"},{"key":"e_1_2_1_2_24_2","unstructured":"FMCSA (2005) Forward Collision Warning Systems (CWS). http:\/\/www.fmcsa.dot.gov\/facts-research\/research-technology\/report\/forward-collision-warning-systems.htm"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Gerth R Peled D Vardi MY Wolper P (1995) Simple on-the-fly automatic verification of linear temporal logic. In: Protocol specification testing and verification pp 3\u201318","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"e_1_2_1_2_26_2","unstructured":"Hamann A Jersak M Richter K Ernst R (2004) Design space exploration and system optimization with SymTA\/S\u2014symbolic timing analysis for systems. In: IEEE real-time systems symposium pp 469\u2013478"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Jonsson J Shin KG (1997) Deadline assignment in distributed hard real-time systems with relaxed locality constraints. In: Distributed computing systems pp 432\u2013440","DOI":"10.1109\/ICDCS.1997.598077"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Konrad S Cheng BHC (2005) Realtime specification patterns. In International conference on software engineering pp 372\u2013381","DOI":"10.1145\/1062455.1062526"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Klobedanz K Kuznik C Thuy A Mueller W (2010) Timing modeling and analysis for AUTOSAR-based software development\u2014a case study. In: Design automation and test in Europe pp 642\u2013645","DOI":"10.1109\/DATE.2010.5457125"},{"volume-title":"Decision procedures, an algorithmic point of view","year":"2008","author":"Kroening D","key":"e_1_2_1_2_30_2"},{"key":"e_1_2_1_2_31_2","unstructured":"Kuntz S (2009) The TIMMO methodology. Technical report Continental Automotive GmbH. http:\/\/www.timmo-2-use.org\/timmo\/pdf\/060409_TIMMO_Methodology.pdf"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018998524196"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Metzner A Franzle M Herde C Stierand I (2005) Scheduling distributed real-time systems by satisfiability checking. In: IEEE conference on embedded and real-time computing systems and applications pp 409\u2013415","DOI":"10.1109\/RTCSA.2005.90"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Di Natale M Stankovic JA (1994) Dynamic end-to-end guarantees in distributed real time systems. In: Real-time systems symposium pp 216\u2013227","DOI":"10.1109\/REAL.1994.342714"},{"key":"e_1_2_1_2_35_2","unstructured":"Peper C Gotzhein R Kronenburg M (1997) Kronenburg: formal specification of real-time requirements for building automation systems. Technical report Report 01\/97 CS Dept University of Kaiserslautern"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: 18th IEEE foundations of computer science pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.39"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0273-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0273-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0273-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T02:07:03Z","timestamp":1745978823000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0273-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,5]]}},"alternative-id":["10.1007\/s00165-012-0273-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0273-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2014,5]]}}}