{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:49:47Z","timestamp":1750308587267,"version":"3.41.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,3,11]],"date-time":"2016-03-11T00:00:00Z","timestamp":1457654400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2016,6,7]]},"abstract":"<jats:p>Building abstract system-level models that faithfully capture performance and functional behavior for embedded systems design is challenging. Unlike functional aspects, performance details are rarely available during the early design phases, and no clear method is known to characterize them. Moreover, once such models are built, they are inherently complex as they mix software models, hardware constraints, and environment abstractions. Their analysis by using traditional performance evaluation methods is reaching the limit. In this article, we present a systematic approach for building stochastic abstract performance models using statistical inference and model calibration, and we propose statistical model checking as a scalable performance evaluation technique for them.<\/jats:p>","DOI":"10.1145\/2885498","type":"journal-article","created":{"date-parts":[[2016,3,14]],"date-time":"2016-03-14T13:24:02Z","timestamp":1457961842000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["<i>ASTROLABE<\/i>"],"prefix":"10.1145","volume":"15","author":[{"given":"Ayoub","family":"Nouri","sequence":"first","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes, VERIMAG, F-38000 Grenoble, France"}]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[{"name":"CNRS, VERIMAG, F-38000 Grenoble, France"}]},{"given":"Anca","family":"Molnos","sequence":"additional","affiliation":[{"name":"CEA\/LETI, Grenoble, France"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[{"name":"INRIA\/IRISA, Rennes, France"}]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Grenoble Alpes, VERIMAG, F-38000 Grenoble, France"}]}],"member":"320","published-online":{"date-parts":[[2016,3,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1166\/jolpe.2009.1040"},{"volume-title":"The New Statistical Analysis of Data","author":"Anderson T. W.","key":"e_1_2_1_2_1","unstructured":"T. W. Anderson . 1996. The New Statistical Analysis of Data . Springer . T. W. Anderson. 1996. The New Statistical Analysis of Data. Springer."},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"L. A\u015ftef\u0103noaei S. B. Rayana S. Bensalem M. Bozga and J. Combaz. 2014. Compositional invariant generation for timed systems. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14). Springer 263--278.  L. A\u015ftef\u0103noaei S. B. Rayana S. Bensalem M. Bozga and J. Combaz. 2014. Compositional invariant generation for timed systems. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14). Springer 263--278.","DOI":"10.1007\/978-3-642-54862-8_18"},{"key":"e_1_2_1_4_1","unstructured":"C. Baier and J. P. Katoen. 2008. Principles of Model Checking. MIT Press.   C. Baier and J. P. Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/384197.384210"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2011.27"},{"volume-title":"10th International Symposium (FMCO'11)","author":"Basu A.","key":"e_1_2_1_7_1","unstructured":"A. Basu , S. Bensalem , M. Bozga , P. Bourgos , M. Maheshwari , and J. Sifakis . 2011a. Component assemblies in the context of manycore. In Formal Methods for Components and Objects , 10th International Symposium (FMCO'11) . 314--333. A. Basu, S. Bensalem, M. Bozga, P. Bourgos, M. Maheshwari, and J. Sifakis. 2011a. Component assemblies in the context of manycore. In Formal Methods for Components and Objects, 10th International Symposium (FMCO'11). 314--333."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"G. Behrmann A. David and K. G. Larsen. 2004. A tutorial on Uppaal. In Formal Methods for the Design of Computer Communication and Software Systems (SFM-RT'04). 200--236.  G. Behrmann A. David and K. G. Larsen. 2004. A tutorial on Uppaal. In Formal Methods for the Design of Computer Communication and Software Systems (SFM-RT'04). 200--236.","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34026-0_25"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-012-0168-6"},{"key":"e_1_2_1_11_1","unstructured":"P. Bourgos. 2013. Rigorous Design Flow for Programming Manycore Platforms. Ph. D. Dissertation. Universit\u00e9 de Grenoble. https:\/\/tel.archives-ouvertes.fr\/tel-01135186.  P. Bourgos. 2013. Rigorous Design Flow for Programming Manycore Platforms. Ph. D. Dissertation. Universit\u00e9 de Grenoble. https:\/\/tel.archives-ouvertes.fr\/tel-01135186."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1970.10481180"},{"volume-title":"Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL'12)","author":"Bulychev P. E.","key":"e_1_2_1_13_1","unstructured":"P. E. Bulychev , A. David , K. G. Larsen , M. Mikucionis , D. B. Poulsen , A. Legay , and Z. Wang . 2012. UPPAAL-SMC: Statistical model checking for priced timed automata . In Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL'12) . 1--16. P. E. Bulychev, A. David, K. G. Larsen, M. Mikucionis, D. B. Poulsen, A. Legay, and Z. Wang. 2012. UPPAAL-SMC: Statistical model checking for priced timed automata. In Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL'12). 1--16."},{"volume-title":"Statistical Data Analysis","author":"Cowan G.","key":"e_1_2_1_14_1","unstructured":"G. Cowan . 1998. Statistical Data Analysis . Oxford University Press , Oxford . G. Cowan. 1998. Statistical Data Analysis. Oxford University Press, Oxford."},{"volume-title":"International Workshop on Worst-Case Execution Time Analysis (WCET'10)","author":"Dalsgaard A. E.","key":"e_1_2_1_15_1","unstructured":"A. E. Dalsgaard , M. C. Olesen , M. Toft , R. R. Hansen , and K. G. Larsen . 2010. METAMOC: Modular execution time analysis using model checking . In International Workshop on Worst-Case Execution Time Analysis (WCET'10) . 113--123. A. E. Dalsgaard, M. C. Olesen, M. Toft, R. R. Hansen, and K. G. Larsen. 2010. METAMOC: Modular execution time analysis using model checking. In International Workshop on Worst-Case Execution Time Analysis (WCET'10). 113--123."},{"key":"e_1_2_1_16_1","volume-title":"Fitdistrplus: Help to Fit of a Parametric Distribution to Non-Censored or Censored Data.","author":"Delignette-Muller M. L.","year":"2010","unstructured":"M. L. Delignette-Muller , R. Pouillot , J.-B. Denis , and C. Dutang . 2010 . Fitdistrplus: Help to Fit of a Parametric Distribution to Non-Censored or Censored Data. Retrieved from http:\/\/cran.r-project.org\/package=fitdistrplus. M. L. Delignette-Muller, R. Pouillot, J.-B. Denis, and C. Dutang. 2010. Fitdistrplus: Help to Fit of a Parametric Distribution to Non-Censored or Censored Data. Retrieved from http:\/\/cran.r-project.org\/package=fitdistrplus."},{"volume-title":"Proceedings of Design, Automation and Test in Europe (DATE'01)","author":"Giusto P.","key":"e_1_2_1_17_1","unstructured":"P. Giusto , G. Martin , and E. Harcourt . 2001. Reliable estimation of execution time of embedded software . In Proceedings of Design, Automation and Test in Europe (DATE'01) . IEEE Press, 580--589. P. Giusto, G. Martin, and E. Harcourt. 2001. Reliable estimation of execution time of embedded software. In Proceedings of Design, Automation and Test in Europe (DATE'01). IEEE Press, 580--589."},{"volume-title":"International Conference on Systems, Architectures, Modeling and Simulation (SAMOS'09)","author":"Haid W.","key":"e_1_2_1_18_1","unstructured":"W. Haid , M. Keller , K. Huang , I. Bacivarov , and L. Thiele . 2009. Generation and calibration of compositional performance analysis models for multi-processor systems . In International Conference on Systems, Architectures, Modeling and Simulation (SAMOS'09) . 92--99. W. Haid, M. Keller, K. Huang, I. Bacivarov, and L. Thiele. 2009. Generation and calibration of compositional performance analysis models for multi-processor systems. In International Conference on Systems, Architectures, Modeling and Simulation (SAMOS'09). 92--99."},{"volume-title":"IEEE Proceedings Computers and Digital Techniques.","author":"Henia R.","key":"e_1_2_1_19_1","unstructured":"R. Henia , A. Hamann , M. Jersak , R. Racu , K. Richter , and R. Ernst . 2005. System level performance analysis - the SymTA\/S approach . In IEEE Proceedings Computers and Digital Techniques. R. Henia, A. Hamann, M. Jersak, R. Racu, K. Richter, and R. Ernst. 2005. System level performance analysis - the SymTA\/S approach. In IEEE Proceedings Computers and Digital Techniques."},{"volume-title":"International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04)","author":"H\u00e9rault T.","key":"e_1_2_1_20_1","unstructured":"T. H\u00e9rault , R. Lassaigne , F. Magniette , and S. Peyronnet . 2004. Approximate probabilistic model checking . In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04) . 73--84. T. H\u00e9rault, R. Lassaigne, F. Magniette, and S. Peyronnet. 2004. Approximate probabilistic model checking. In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04). 73--84."},{"key":"e_1_2_1_21_1","volume-title":"IFIP Congress. 471--475","author":"Kahn G.","year":"1974","unstructured":"G. Kahn . 1974 . The semantics of simple language for parallel programming . In IFIP Congress. 471--475 . G. Kahn. 1974. The semantics of simple language for parallel programming. In IFIP Congress. 471--475."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.898830"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"B. Kienhuis E. F. Deprettere P. van der Wolf and K. A. Vissers. 2002. A methodology to design programmable embedded systems - the Y-chart approach. In Embedded Processor Design Challenges: Systems Architectures Modeling and Simulation (SAMOS'02). Springer-Verlag London 18--37.   B. Kienhuis E. F. Deprettere P. van der Wolf and K. A. Vissers. 2002. A methodology to design programmable embedded systems - the Y-chart approach. In Embedded Processor Design Challenges: Systems Architectures Modeling and Simulation (SAMOS'02). Springer-Verlag London 18--37.","DOI":"10.1007\/3-540-45874-3_2"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1530873.1530882"},{"volume-title":"Performance Evaluation of Computer and Communication Systems","author":"Le Boudec J.-Y.","key":"e_1_2_1_25_1","unstructured":"J.-Y. Le Boudec . 2010. Performance Evaluation of Computer and Communication Systems . EPFL Press , Lausanne, Switzerland . J.-Y. Le Boudec. 2010. Performance Evaluation of Computer and Communication Systems. EPFL Press, Lausanne, Switzerland."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/65.2.297"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2011.21"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"H. Mao Y. Chen M. Jaeger T. D. Nielsen K. G. Larsen and B. Nielsen. 2012. Learning Markov decision processes for model checking. Quantities in Formal Methods (QFM'12). 49--63.  H. Mao Y. Chen M. Jaeger T. D. Nielsen K. G. Larsen and B. Nielsen. 2012. Learning Markov decision processes for model checking. Quantities in Formal Methods (QFM'12). 49--63.","DOI":"10.4204\/EPTCS.103.6"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228568"},{"volume-title":"Proceedings of the IEEE International ASIC\/SOC Conference.","author":"Mohanty S.","key":"e_1_2_1_30_1","unstructured":"S. Mohanty and V. K. Prasanna . 2002. Rapid system-level performance evaluation and optimization for application mapping onto SoC architectures . In Proceedings of the IEEE International ASIC\/SOC Conference. S. Mohanty and V. K. Prasanna. 2002. Rapid system-level performance evaluation and optimization for application mapping onto SoC architectures. In Proceedings of the IEEE International ASIC\/SOC Conference."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11263-007-0118-0"},{"key":"e_1_2_1_32_1","unstructured":"A. Nouri. 2015. Rigorous System-Level Modeling and Performance Evaluation for Embedded System Design. Ph. D. Dissertation. Universit\u00e9 Grenoble Alpes.  A. Nouri. 2015. Rigorous System-Level Modeling and Performance Evaluation for Embedded System Design. Ph. D. Dissertation. Universit\u00e9 Grenoble Alpes."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0313-6"},{"volume-title":"Proceedings of the 12th ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'14)","author":"Nouri A.","key":"e_1_2_1_34_1","unstructured":"A. Nouri , M. Bozga , A. Molnos , A. Legay , and S. Bensalem . 2014a. Building faithful high-level models and performance evaluation of manycore embedded systems . In Proceedings of the 12th ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'14) . IEEE, 209--218. A. Nouri, M. Bozga, A. Molnos, A. Legay, and S. Bensalem. 2014a. Building faithful high-level models and performance evaluation of manycore embedded systems. In Proceedings of the 12th ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE'14). IEEE, 209--218."},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","unstructured":"A. Nouri B. Raman M. Bozga A. Legay and S. Bensalem. 2014b. Faster statistical model checking by means of abstraction and learning. In Runtime Verification - 5th International Conference (RV'14). Springer 340--355.  A. Nouri B. Raman M. Bozga A. Legay and S. Bensalem. 2014b. Faster statistical model checking by means of abstraction and learning. In Runtime Verification - 5th International Conference (RV'14). Springer 340--355.","DOI":"10.1007\/978-3-319-11164-3_28"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1504\/IJES.2008.020299"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2006.16"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11265-007-0085-2"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2007.53"},{"key":"e_1_2_1_41_1","volume-title":"International Symposium on Circuits and Systems (ISCAS'00)","volume":"4","author":"Thiele L.","unstructured":"L. Thiele , S. Chakraborty , and M. Naedele . 2000. Real-time calculus for scheduling hard real-time systems . In International Symposium on Circuits and Systems (ISCAS'00) , Vol. 4 . 101--104. L. Thiele, S. Chakraborty, and M. Naedele. 2000. Real-time calculus for scheduling hard real-time systems. In International Symposium on Circuits and Systems (ISCAS'00), Vol. 4. 101--104."},{"key":"e_1_2_1_42_1","volume-title":"Risk Analysis: A Quantitative Guide","author":"Vose D.","year":"2008","unstructured":"D. Vose . 2008 . Risk Analysis: A Quantitative Guide . Wiley . D. Vose. 2008. Risk Analysis: A Quantitative Guide. Wiley."},{"key":"e_1_2_1_43_1","unstructured":"H. L. S. Younes. 2005. Verification and Planning for Stochastic Processes with Asynchronous Events. Ph. D. Dissertation. Carnegie Mellon.   H. L. S. Younes. 2005. Verification and Planning for Stochastic Processes with Asynchronous Events. Ph. D. Dissertation. Carnegie Mellon."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2885498","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2885498","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:14Z","timestamp":1750273514000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2885498"}},"subtitle":["A Rigorous Approach for System-Level Performance Modeling and Analysis"],"short-title":[],"issued":{"date-parts":[[2016,3,11]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,6,7]]}},"alternative-id":["10.1145\/2885498"],"URL":"https:\/\/doi.org\/10.1145\/2885498","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2016,3,11]]},"assertion":[{"value":"2015-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-03-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}