{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T10:46:21Z","timestamp":1761648381890,"version":"3.41.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2016,6,24]],"date-time":"2016-06-24T00:00:00Z","timestamp":1466726400000},"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":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2016,6,24]]},"abstract":"<jats:p>The dependency on the correct functioning of embedded systems is rapidly growing, mainly due to their wide range of applications, such as micro-grids, automotive device control (e.g., airbag control), health care, surveillance, mobile devices, and consumer electronics. Their structures are becoming more and more complex and now require multi-core processors with scalable shared memory, in order to meet increasing computational power demands. As a consequence, reliability of embedded (distributed) software becomes a key issue during system development, which must be carefully addressed and assured. Normally, state-of-the-art verification methodologies for embedded systems generate test vectors (with constraints) and use assertion-based verification and highlevel processor models, during simulation; however, other additional challenges have been raised: the need for meeting time and energy constraints, handling concurrent software, dealing with platform restrictions, evaluating implementation-structure choices, and supporting new software architectures and legacy designs (usually written in low-level languages). The present paper discusses challenges, problems, and recent advances to ensure correctness and timeliness regarding embedded systems. Reliability issues, in the development of micro-grids and cyber-physical systems, are then considered, as a prominent (bounded) model checking application.<\/jats:p>","DOI":"10.1145\/2934240.2934247","type":"journal-article","created":{"date-parts":[[2016,6,27]],"date-time":"2016-06-27T13:41:38Z","timestamp":1467034898000},"page":"1-6","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["SMT-Based Context-Bounded Model Checking for Embedded Systems"],"prefix":"10.1145","volume":"41","author":[{"given":"Lucas C.","family":"Cordeiro","sequence":"first","affiliation":[{"name":"Federal University of Amazonas, Brazil"}]},{"given":"Eddie B.","family":"de Lima Filho","sequence":"additional","affiliation":[{"name":"Science, Technology, and Innovation Center for the Industrial Pole of Manaus, Brazil"}]}],"member":"320","published-online":{"date-parts":[[2016,6,24]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"4419","article-title":"Real-Time Systems - Design Principles for Distributed Embedded Applications. Real-Time Systems Series, Springer","volume":"978","author":"Kopetz","year":"2011","journal-title":"ISBN"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Xua X. Jiaa H. Wanga D. Yub D. Chiangc H.: Hierarchical energy management system for multi-source multi-product microgrids In: Renewable Energy v. 78 pp. 621--630 2015.  Xua X. Jiaa H. Wanga D. Yub D. Chiangc H.: Hierarchical energy management system for multi-source multi-product microgrids In: Renewable Energy v. 78 pp. 621--630 2015.","DOI":"10.1016\/j.renene.2015.01.039"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2008.25"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.3390\/s150304837"},{"key":"e_1_2_1_5_1","first-page":"233","volume-title":"Springer","author":"Groza A.","year":"2015"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICESS.2009.82"},{"key":"e_1_2_1_7_1","first-page":"1","volume-title":"Lin S.: Cyber Physical System Challenges for Human-in-the-Loop Control. In: 8th International Workshop on Feedback Computing","author":"Munir S.","year":"2013"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/2755753.2755803"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/646483.691738"},{"key":"e_1_2_1_10_1","unstructured":"Biere\n       \n      A. Heule\n       \n      M. van Maaren\n       \n      H. Walsh\n       \n      T. eds.: \n  Handbook of Satisfiability\n  . Volume \n  185\n   of \n  Frontiers in Artifcial Intelligence and Applications\n  . IOS Press 2009\n  .   Biere A. Heule M. van Maaren H. Walsh T. eds.: Handbook of Satisfiability. Volume 185 of Frontiers in Artifcial Intelligence and Applications. IOS Press 2009."},{"key":"e_1_2_1_11_1","unstructured":"Barrett\n       \n      C. Sebastiani\n       \n      R. Seshia\n       \n      S.A. Tinelli\n       \n      C.\n      \n  \n  : \n  Satisfiability Modulo Theories\n  . In: Volume \n  185\n   of \n  Frontiers in Artificial Intelligence and Applications\n  . \n  IOS Press pp. \n  825\n  --\n  885 2009\n  .  Barrett C. Sebastiani R. Seshia S.A. Tinelli C.: Satisfiability Modulo Theories. In: Volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press pp. 825--885 2009."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691617_9"},{"key":"e_1_2_1_13_1","first-page":"168","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems. LNCS 2988","author":"Clarke E.","year":"2004"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_12"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985839"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2005.77"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.59"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/646186.683237"},{"key":"e_1_2_1_20_1","first-page":"1","article-title":"The calculus of computation - decision procedures with applications to verification. In: Springer, pp","author":"Bradley A.","year":"2007","journal-title":"I-XV"},{"key":"e_1_2_1_21_1","unstructured":"ParisTech M.: PIPS: Automatic Parallelizer and Code Transformation Framework. Accessed 21 February 2016  ParisTech M.: PIPS: Automatic Parallelizer and Code Transformation Framework. Accessed 21 February 2016"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.11.003"},{"volume-title":"International Journal on Software Tools for Technology Transfer (to appear)","year":"2015","author":"Gadelha M.","key":"e_1_2_1_23_1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_9"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SBESC.2015.24"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041578"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1941553.1941604"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/MTV.2009.16"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10836-015-5518-4"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23404-5_9"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1874620.1874912"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_25"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_31"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_39"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2013.15"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2851613.2851830"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/GCCE.2015.7398699"},{"volume-title":"PhD Thesis","year":"2015","author":"Morse","key":"e_1_2_1_39_1"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.99"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040316"},{"first-page":"1","volume-title":"McMillan: Widening and Interpolation. In: International Symposium on Static Analysis, LCNS 6887","year":"2011","key":"e_1_2_1_42_1"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/IECON.2014.7048514"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.14209\/sbrt.2013.178"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-013-0366-0"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10617-016-9173-5"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_47"},{"key":"e_1_2_1_48_1","first-page":"405","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems. LNCS 8413","author":"Morse J.","year":"2014"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_31"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/SBESC.2015.25"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-32582-8_6"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786867"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30729-4_10"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2934240.2934247","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2934240.2934247","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:54:54Z","timestamp":1750222494000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2934240.2934247"}},"subtitle":["Challenges and Future Trends"],"short-title":[],"issued":{"date-parts":[[2016,6,24]]},"references-count":53,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,6,24]]}},"alternative-id":["10.1145\/2934240.2934247"],"URL":"https:\/\/doi.org\/10.1145\/2934240.2934247","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2016,6,24]]},"assertion":[{"value":"2016-06-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}