{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:26:10Z","timestamp":1740122770008,"version":"3.37.3"},"reference-count":59,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,2,21]],"date-time":"2017-02-21T00:00:00Z","timestamp":1487635200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100012913","name":"TATA CONSULTANCY SERVICES","doi-asserted-by":"crossref","award":["TCS Research Fellowship Cycle 8"],"award-info":[{"award-number":["TCS Research Fellowship Cycle 8"]}],"id":[{"id":"10.13039\/100012913","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Des Autom Embed Syst"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s10617-017-9183-y","type":"journal-article","created":{"date-parts":[[2017,2,21]],"date-time":"2017-02-21T05:56:55Z","timestamp":1487656615000},"page":"37-87","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["RELSPEC: a framework for reliability aware design of component based embedded systems"],"prefix":"10.1007","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9049-9455","authenticated-orcid":false,"given":"Saurav Kumar","family":"Ghosh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.","family":"Vishnuvardhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Satya Gautam","family":"Vadlamudi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aritra","family":"Hazra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Soumyajit","family":"Dey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Partha Pratim","family":"Chakrabarti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,21]]},"reference":[{"key":"9183_CR1","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP et al (2008) Principles of model checking, vol 26202649. MIT Press, Cambridge"},{"key":"9183_CR2","doi-asserted-by":"crossref","unstructured":"Ball T, Majumdar R, Millstein T, Rajamani SK (2001) Automatic predicate abstraction of c programs. In: Programming language design and implementation. ACM, pp 203\u2013213","DOI":"10.1145\/378795.378846"},{"key":"9183_CR3","doi-asserted-by":"crossref","unstructured":"Bonami P, Kilin\u00e7 M, Linderoth J (2012) Algorithms and software for convex mixed integer nonlinear programs. In: Mixed integer nonlinear programming. Springer, Berlin, pp 1\u201339","DOI":"10.1007\/978-1-4614-1927-3_1"},{"issue":"13","key":"9183_CR4","first-page":"5","volume":"14","author":"G Booch","year":"1996","unstructured":"Booch G, Rumbaugh J, Jacobson I (1996) The unified modeling language. Unix Rev 14(13):5","journal-title":"Unix Rev"},{"issue":"10","key":"9183_CR5","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1145\/2544173.2509546","volume":"48","author":"M Carbin","year":"2013","unstructured":"Carbin M, Misailovic S, Rinard MC (2013) Verifying quantitative reliability for programs that execute on unreliable hardware. ACM SIGPLAN Not 48(10):33\u201352","journal-title":"ACM SIGPLAN Not"},{"issue":"11","key":"9183_CR6","doi-asserted-by":"crossref","first-page":"2213","DOI":"10.1016\/j.disc.2007.04.067","volume":"308","author":"Y Cheng","year":"2008","unstructured":"Cheng Y, Sun X, Yin YL (2008) Searching monotone multi-dimensional arrays. Discrete Math 308(11):2213\u20132221","journal-title":"Discrete Math"},{"issue":"2","key":"9183_CR7","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1109\/TSE.1980.234477","volume":"6","author":"RC Cheung","year":"1980","unstructured":"Cheung RC (1980) A user-oriented software reliability model. IEEE Trans Softw Eng 6(2):118\u2013125","journal-title":"IEEE Trans Softw Eng"},{"key":"9183_CR8","doi-asserted-by":"crossref","unstructured":"Cuoq P, Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B (2012) Frama-c. In: Software engineering and formal methods. Springer, Berlin, pp 233\u2013247","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"9183_CR9","doi-asserted-by":"crossref","unstructured":"Day TD, Roberts SG (2002) A simulation model for vehicle braking systems fitted with abs. Tech. rep, SAE Technical Paper","DOI":"10.4271\/2002-01-0559"},{"issue":"4","key":"9183_CR10","doi-asserted-by":"crossref","first-page":"1273","DOI":"10.1016\/j.jsc.2003.04.003","volume":"38","author":"JA Loera De","year":"2004","unstructured":"De Loera JA, Hemmecke R, Tauzer J, Yoshida R (2004) Effective lattice point counting in rational convex polytopes. J Symb Comput 38(4):1273\u20131302","journal-title":"J Symb Comput"},{"issue":"8","key":"9183_CR11","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra EW (1975) Guarded commands, nondeterminacy and formal derivation of programs. Commun ACM 18(8):453\u2013457","journal-title":"Commun ACM"},{"issue":"1","key":"9183_CR12","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/0164-1212(88)90043-X","volume":"8","author":"WH Farr","year":"1988","unstructured":"Farr WH, Smith OD (1988) A tool for statistical modeling and estimation of reliability functions for software: Smerfs. J Syst Softw 8(1):47\u201355","journal-title":"J Syst Softw"},{"issue":"3","key":"9183_CR13","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/373243.360220","volume":"36","author":"C Flanagan","year":"2001","unstructured":"Flanagan C, Saxe JB (2001) Avoiding exponential explosion: generating compact verification conditions. ACM SIGPLAN Not 36(3):193\u2013205","journal-title":"ACM SIGPLAN Not"},{"key":"9183_CR14","doi-asserted-by":"crossref","unstructured":"Ghosh SK, Hazra A, Dey S (2015) Relspec: a framework for early reliability refinement of embedded applications. In: International conference on VLSI design. IEEE, pp 41\u201346","DOI":"10.1109\/VLSID.2015.12"},{"key":"9183_CR15","unstructured":"Gokhale S, Trivedi KS (1997) Structure-based software reliability prediction. In: International conference on advanced computing. Citeseer"},{"issue":"1","key":"9183_CR16","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1109\/TDSC.2007.4","volume":"4","author":"SS Gokhale","year":"2007","unstructured":"Gokhale SS (2007) Architecture-based software reliability analysis: overview and limitations. IEEE Trans Dependable Secure Comput 4(1):32\u201340","journal-title":"IEEE Trans Dependable Secure Comput"},{"key":"9183_CR17","doi-asserted-by":"crossref","unstructured":"Gokhale SS, Trivedi KS (2002) Reliability prediction and sensitivity analysis based on software architecture. In: International symposium on software reliability engineering. IEEE, pp 64\u201375","DOI":"10.1109\/ISSRE.2002.1173214"},{"key":"9183_CR18","doi-asserted-by":"crossref","unstructured":"Gokhale SS, Wong WE, Trivedi KS, Horgan J (1998) An analytical approach to architecture-based software reliability prediction. In: International computer performance and dependability symposium. IEEE, pp 13\u201322","DOI":"10.1109\/IPDS.1998.707705"},{"key":"9183_CR19","doi-asserted-by":"crossref","unstructured":"Goseva-Popstojanova K, Mathur AP, Trivedi KS (2001) Comparison of architecture-based software reliability models. In: International symposium on software reliability engineering. IEEE, pp 22\u201331","DOI":"10.1109\/ISSRE.2001.989455"},{"issue":"2","key":"9183_CR20","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/S0166-5316(01)00034-7","volume":"45","author":"K Go\u0161eva-Popstojanova","year":"2001","unstructured":"Go\u0161eva-Popstojanova K, Trivedi KS (2001) Architecture-based approach to reliability assessment of software systems. Perform Eval 45(2):179\u2013204","journal-title":"Perform Eval"},{"key":"9183_CR21","doi-asserted-by":"crossref","unstructured":"Gupta A, Rybalchenko A (2009) Invgen: An efficient invariant generator. In: Computer aided verification. Springer, Berlin, pp 634\u2013640","DOI":"10.1007\/978-3-642-02658-4_48"},{"key":"9183_CR22","doi-asserted-by":"crossref","unstructured":"Gustafsson J, Ermedahl A, Sandberg C, Lisper B (2006) Automatic derivation of loop bounds and infeasible paths for WCET analysis using abstract execution. In: International real-time systems symposium. IEEE, pp 57\u201366","DOI":"10.1109\/RTSS.2006.12"},{"issue":"1","key":"9183_CR23","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/LES.2013.2239605","volume":"5","author":"A Hazra","year":"2013","unstructured":"Hazra A, Ghosh P, Vadlamudi SG, Chakrabarti PP, Dasgupta P (2013) Formal methods for early analysis of functional reliability in component-based embedded applications. Embed Syst Lett 5(1):8\u201311","journal-title":"Embed Syst Lett"},{"issue":"1","key":"9183_CR24","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1109\/TR.2011.2104490","volume":"60","author":"CJ Hsu","year":"2011","unstructured":"Hsu CJ, Huang CY (2011) An adaptive reliability analysis using path testing for complex component-based software systems. IEEE Trans Reliab 60(1):158\u2013170","journal-title":"IEEE Trans Reliab"},{"issue":"1","key":"9183_CR25","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s10270-006-0040-x","volume":"7","author":"A Immonen","year":"2008","unstructured":"Immonen A, Niemel\u00e4 E (2008) Survey of reliability and availability prediction methods from the viewpoint of software architecture. Softw Syst Model 7(1):49\u201365","journal-title":"Softw Syst Model"},{"issue":"2","key":"9183_CR26","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1016\/S0167-6423(96)00019-6","volume":"28","author":"H Jifeng","year":"1997","unstructured":"Jifeng H, Seidel K, McIver A (1997) Probabilistic models for the guarded command language. Sci Comput Program 28(2):171\u2013192","journal-title":"Sci Comput Program"},{"issue":"1","key":"9183_CR27","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1109\/JPROC.2002.805824","volume":"91","author":"G Karsai","year":"2003","unstructured":"Karsai G, Sztipanovits J, Ledeczi A, Bapty T (2003) Model-integrated development of embedded software. Proc IEEE 91(1):145\u2013164","journal-title":"Proc IEEE"},{"key":"9183_CR28","volume-title":"Fault-tolerant systems","author":"I Koren","year":"2010","unstructured":"Koren I, Krishna CM (2010) Fault-tolerant systems. Morgan Kaufmann, Los Altos"},{"key":"9183_CR29","doi-asserted-by":"crossref","unstructured":"Krishnamurthy S, Mathur AP (1997) On the estimation of reliability of a software system using reliabilities of its components. In: International symposium on software reliability engineering. IEEE, pp 146\u2013155","DOI":"10.1109\/ISSRE.1997.630860"},{"issue":"1","key":"9183_CR30","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0167-6377(89)90031-X","volume":"8","author":"P Kubat","year":"1989","unstructured":"Kubat P (1989) Assessing reliability of modular software. Oper Res Lett 8(1):35\u201341","journal-title":"Oper Res Lett"},{"key":"9183_CR31","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: Verification of probabilistic real-time systems. In: Computer aided verification. Springer, Berlin, pp 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"9183_CR32","unstructured":"Labuhn PI, Chundrlik Jr WJ (1995) Adaptive cruise control. US Patent 5,454,442"},{"issue":"6","key":"9183_CR33","doi-asserted-by":"crossref","first-page":"701","DOI":"10.1109\/TSE.1984.5010299","volume":"10","author":"JC Laprie","year":"1984","unstructured":"Laprie JC (1984) Dependability evaluation of software systems in operation. IEEE Trans Softw Eng 10(6):701\u2013714","journal-title":"IEEE Trans Softw Eng"},{"issue":"2","key":"9183_CR34","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1109\/24.784274","volume":"48","author":"J Ledoux","year":"1999","unstructured":"Ledoux J (1999) Availability modeling of modular software. IEEE Trans Reliab 48(2):159\u2013168","journal-title":"IEEE Trans Reliab"},{"issue":"6","key":"9183_CR35","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"KRM Leino","year":"2005","unstructured":"Leino KRM (2005) Efficient weakest preconditions. Inf Process Lett 93(6):281\u2013288","journal-title":"Inf Process Lett"},{"key":"9183_CR36","doi-asserted-by":"crossref","unstructured":"Li C, Zhou X, Wang Y, Dong Y (2009) An improved path-based reliability prediction model for component-based embedded software. In: International conference on frontier of computer science and technology. IEEE, pp 301\u2013307","DOI":"10.1109\/FCST.2009.83"},{"issue":"2","key":"9183_CR37","doi-asserted-by":"crossref","first-page":"172","DOI":"10.2307\/2346564","volume":"24","author":"B Littlewood","year":"1975","unstructured":"Littlewood B (1975) A reliability model for systems with markov structure. Appl Stat 24(2):172\u2013177","journal-title":"Appl Stat"},{"issue":"3","key":"9183_CR38","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1109\/TR.1979.5220576","volume":"28","author":"B Littlewood","year":"1979","unstructured":"Littlewood B (1979) Software reliability model for modular program structure. IEEE Trans Reliab 28(3):241\u2013246","journal-title":"IEEE Trans Reliab"},{"issue":"3","key":"9183_CR39","doi-asserted-by":"crossref","first-page":"332","DOI":"10.2307\/2346781","volume":"22","author":"B Littlewood","year":"1973","unstructured":"Littlewood B, Verrall J (1973) A bayesian reliability growth model for computer software. Appl Stat 22(3):332\u2013346","journal-title":"Appl Stat"},{"key":"9183_CR40","doi-asserted-by":"crossref","unstructured":"Lohar D, Dey S (2015) Integrating formal methods with testing for reliability estimation of component based systems. In: International symposium on software reliability engineering, p. to appear. IEEE","DOI":"10.1109\/ISSREW.2015.7392033"},{"key":"9183_CR41","doi-asserted-by":"crossref","unstructured":"Lyu MR, Nikora A (1992) Casre: a computer-aided software reliability estimation tool. In: International workshop on computer-aided software engineering. IEEE, pp 264\u2013275","DOI":"10.1109\/CASE.1992.200165"},{"key":"9183_CR42","unstructured":"Lyu MR, et\u00a0al (1996) Handbook of software reliability engineering, vol 222. IEEE Computer Society Press, CA"},{"issue":"4","key":"9183_CR43","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1109\/TR.2002.804489","volume":"51","author":"YK Malaiya","year":"2002","unstructured":"Malaiya YK, Li MN, Bieman JM, Karcich R (2002) Software reliability growth with test coverage. IEEE Trans Reliab 51(4):420\u2013426","journal-title":"IEEE Trans Reliab"},{"key":"9183_CR44","doi-asserted-by":"crossref","unstructured":"Malakova M, Dimov A, Dimov D (2012) Soregene: a software reliability modelling tool. In: International conference on computer systems and technologies. ACM, pp 179\u2013186","DOI":"10.1145\/2383276.2383304"},{"key":"9183_CR45","unstructured":"MathWorks: Model-Based Design. www.mathworks.in\/model-based-design\/"},{"key":"9183_CR46","unstructured":"MathWorks: Simulink. www.mathworks.in\/products\/simulink\/"},{"key":"9183_CR47","unstructured":"MathWorks: Stateflow. www.mathworks.in\/products\/stateflow\/"},{"key":"9183_CR48","volume-title":"Software reliability: measurement, prediction, application","author":"JD Musa","year":"1987","unstructured":"Musa JD, Iannino A, Okumoto K (1987) Software reliability: measurement, prediction, application. McGraw-Hill, Inc., NY"},{"key":"9183_CR49","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of program analysis","author":"F Nielson","year":"1999","unstructured":"Nielson F, Nielson HR, Hankin C (1999) Principles of program analysis. Springer, Berlin"},{"key":"9183_CR50","unstructured":"Oldenkamp H (2007) Probabilistic model checking: a comparison of tools. Master\u2019s thesis, University of Twente, Enschede, Netherlands"},{"key":"9183_CR51","doi-asserted-by":"crossref","unstructured":"Pratt VR (1979) Models of program logics. In: Foundations of computer science. IEEE, pp 115\u2013122","DOI":"10.1109\/SFCS.1979.24"},{"key":"9183_CR52","unstructured":"ReliaSoft Corporation: BlockSim. http:\/\/www.reliasoft.com\/BlockSim\/index.html"},{"key":"9183_CR53","volume-title":"Embedded systems and software validation","author":"A Roychoudhury","year":"2009","unstructured":"Roychoudhury A (2009) Embedded systems and software validation. Morgan Kaufmann, Los Altos"},{"issue":"2","key":"9183_CR54","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1109\/TR.1987.5222336","volume":"36","author":"RA Sahner","year":"1987","unstructured":"Sahner RA, Trivedi KS (1987) Reliability modeling using sharpe. IEEE Trans Reliab 36(2):186\u2013193","journal-title":"IEEE Trans Reliab"},{"key":"9183_CR55","unstructured":"Shooman ML (1976) Structural models for software reliability prediction. In: International conference on software engineering. IEEE Computer Society Press, pp 268\u2013280"},{"issue":"1","key":"9183_CR56","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1109\/TDSC.2013.23","volume":"11","author":"SG Vadlamudi","year":"2014","unstructured":"Vadlamudi SG, Chakrabarti PP (2014) Robustness analysis of embedded control systems with respect to signal perturbations: finding minimal counterexamples using fault injection. IEEE Trans Dependable Secure Comput 11(1):45\u201358","journal-title":"IEEE Trans Dependable Secure Comput"},{"issue":"1","key":"9183_CR57","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1016\/j.jss.2005.09.004","volume":"79","author":"WL Wang","year":"2006","unstructured":"Wang WL, Pan D, Chen MH (2006) Architecture-based software reliability modeling. J Syst Softw 79(1):132\u2013146","journal-title":"J Syst Softw"},{"key":"9183_CR58","doi-asserted-by":"crossref","DOI":"10.1142\/1390","volume-title":"Software reliability modelling","author":"M Xie","year":"1991","unstructured":"Xie M (1991) Software reliability modelling, vol 1. World Scientific, Singapore"},{"key":"9183_CR59","doi-asserted-by":"crossref","unstructured":"Yacoub SM, Cukic B, Ammar HH (1999) Scenario-based reliability analysis of component-based software. In: International symposium on software reliability engineering. IEEE, pp 22\u201331","DOI":"10.1109\/ISSRE.1999.809307"}],"container-title":["Design Automation for Embedded Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10617-017-9183-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10617-017-9183-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10617-017-9183-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T16:11:22Z","timestamp":1589731882000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10617-017-9183-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,21]]},"references-count":59,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["9183"],"URL":"https:\/\/doi.org\/10.1007\/s10617-017-9183-y","relation":{},"ISSN":["0929-5585","1572-8080"],"issn-type":[{"type":"print","value":"0929-5585"},{"type":"electronic","value":"1572-8080"}],"subject":[],"published":{"date-parts":[[2017,2,21]]}}}