{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,16]],"date-time":"2023-01-16T23:29:19Z","timestamp":1673911759650},"reference-count":43,"publisher":"Elsevier","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1016\/b978-0-12-385510-7.00006-0","type":"book-chapter","created":{"date-parts":[[2012,3,24]],"date-time":"2012-03-24T17:49:07Z","timestamp":1332611347000},"page":"277-321","source":"Crossref","is-referenced-by-count":2,"title":["Functional and Nonfunctional Design Verification for Embedded Software Systems"],"prefix":"10.1016","author":[{"given":"Arnab","family":"Ray","sequence":"first","affiliation":[]},{"given":"Christopher","family":"Ackermann","sequence":"additional","affiliation":[]},{"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[]},{"given":"Charles","family":"Shelton","sequence":"additional","affiliation":[]},{"given":"Chris","family":"Martin","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0005","unstructured":"A. Wayne Wymore, Model-Based Systems Engineering. ISBN 978\u20130849380129, 1993"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0010","doi-asserted-by":"crossref","unstructured":"D. Harel, E. Gery, Executable object modeling with statecharts, Proceedings of the 18th international Conference on Software Engineering (Berlin, Germany, March 25\u201329, 1996), International Conference on Software Engineering, IEEE Computer Society, Washington, DC, pp. 246\u2013257","DOI":"10.1109\/ICSE.1996.493420"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0015","unstructured":"High Confidence Software and System Needs, Interagency Working Group in Information Technology Research and Development Report, 2001"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0020","unstructured":"Mathworks Simulik. http:\/\/www.mathworks.com\/ products\/simulink\/, 2011"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0025","unstructured":"ASCET. http:\/\/www.etas.com\/en\/products\/ ascet_software_products.php, 2011"},{"issue":"5","key":"10.1016\/B978-0-12-385510-7.00006-0_bb0030","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1109\/MS.2003.1231146","article-title":"The pragmatics of model-driven development","volume":"20","author":"Selic","year":"2003","journal-title":"IEEE Software"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0035","unstructured":"D. Kalish, R. Montague, Logic: Techniques of Formal Reasoning. ISBN 978\u20130195155044, 1980"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0040","unstructured":"A. Meyer, Principles of Functional Verification. ISBN 978\u20130750676175, 2003"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0045","unstructured":"J. Mylopoulus, E. Yu, B. Nixon, L. Chung, Non-Functional Requirements in Software Engineering. ISBN 978\u20130792386667, 1999"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0050","unstructured":"T. Gilb, D. Graham, Software Inspection. ISBN: 978\u20130201631814, 1994"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0055","doi-asserted-by":"crossref","unstructured":"Y. Ken Wong, Modern Software Review\u2014Techniques and Technologies. ISBN: 978\u20131599040134, 2006","DOI":"10.4018\/978-1-59904-013-4"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0060","unstructured":"E. Clarke. O. Grumberg, D. Pereld, Model Checking. ISBN: 978\u20130262032704, 1999"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0065","unstructured":"C. Baier, J. Katoen, K. Larsen, Principles of Model Checking. ISBN: 978\u20130262026499, 2008"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0070","doi-asserted-by":"crossref","unstructured":"Y. Bertot, P. Casteran, Interactive Theorem Proving. ISBN: 978\u20133540208549, 2004","DOI":"10.1007\/978-3-662-07964-5"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0075","doi-asserted-by":"crossref","unstructured":"J. Schumann, Automated Theorem Proving in Software Engineering. ISBN: 978\u20133540679899, 2001","DOI":"10.1007\/978-3-662-22646-9"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0080","unstructured":"C. Chang, R. Lee. Symbolic Logic and Mechanical Theorem Proving. ISBN: 978\u20130121703509, 1973"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0085","article-title":"Symbolic model checking: 10E20 states and beyond. LICS","author":"Burch","year":"1990"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0090","doi-asserted-by":"crossref","DOI":"10.1145\/143165.143235","article-title":"Model checking and abstraction","author":"Clarke","year":"1992"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0095","series-title":"A Decade of Concurrency\u2014Reflections and Perspectives","article-title":"Verification tools for finite-state concurrent systems","volume":"vol. 803","author":"Clarke","year":"1994"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0100","series-title":"Artificial Intelligence and Mathematical Theory of Computation","first-page":"151","article-title":"Model checking vs. theorem proving: a manifesto","author":"Halpern","year":"1991"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0105","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-55602-8_217","article-title":"PVS: a prototype verification system","author":"Owre","year":"1992"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0110","doi-asserted-by":"crossref","unstructured":"L. Moura, S. Owre, H. Ruess, J. Rushby, N. Shankar, M. Sorea, et al., SAL 2, Proceedings of Computer Aided Verification CAV, LNCS 3114, Springer Verlag, pp. 496\u2013500, 2004","DOI":"10.1007\/978-3-540-27813-9_45"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0115","series-title":"The Spin Verification System American Mathematical Society, DIMACS Series, vol. 32","isbn-type":"print","year":"1997","ISBN":"http:\/\/id.crossref.org\/isbn\/0821806807"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0120","first-page":"261","article-title":"dSPIN: a dynamic extension of SPIN","author":"Iosif","year":"1999"},{"issue":"4","key":"10.1016\/B978-0-12-385510-7.00006-0_bb0125","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1592434.1592436","article-title":"Formal methods: practice and experience","volume":"41","author":"Woodcock","year":"2009","journal-title":"ACM Comput. Surv."},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0130","first-page":"56","article-title":"Non-functional requirements analysis modeling for software product lines","author":"Nguyen","year":"2009"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0135","series-title":"International Series in Software Engineering, vol. 5","doi-asserted-by":"crossref","first-page":"476","DOI":"10.1142\/9789812797971","article-title":"Non-functional requirements in software engineering","author":"Chung","year":"1999"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0140","first-page":"21","article-title":"On non-functional requirements","author":"Glinz","year":"2007"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0145","doi-asserted-by":"crossref","DOI":"10.4271\/2008-01-0741","article-title":"Model-Based Design Verification: A Monitor Based Approach","author":"Ackermann","year":"2008"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0150","series-title":"Proceedings of the 4th international Conference on Quality of Software-Architectures: Models and Architectures, Karlsruhe, Germany, October 14\u201317, 2008","first-page":"171","article-title":"Integrating quality-attribute reasoning frameworks in the ArchE design assistant","volume":"vol. 5281","author":"Diaz-Pace","year":"2008"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0155","article-title":"MILAN: a model based integrated simulation framework for design of embedded systems","author":"Bakshi","year":"2001"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0160","doi-asserted-by":"crossref","unstructured":"Felix Bachmann, Len Bass, Mark Klein, Preliminary Design of ArchE: A Software Architecture Design Assistant (CMU\/SEI-2003-TR-021), 2003","DOI":"10.21236\/ADA421618"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0165","doi-asserted-by":"crossref","DOI":"10.1109\/ICECCS.1998.706657","article-title":"Architecture tradeoff analysis method","author":"Kazman","year":"1998"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0170","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/s11219-005-4250-1","article-title":"A basis for evaluating software architecture analysis methods","volume":"13","author":"Kazman","year":"2005","journal-title":"Software Qual. J."},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0175","series-title":"Proceedings of the 7th international Conference on Software Quality (June 09\u201313, 2002)","first-page":"310","article-title":"Extended model-based testing toward high code coverage rate","volume":"vol. 2349","author":"Takahashi","year":"2002"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0180","unstructured":"Reactive Systems Inc. http:\/\/reactive-systems.com, 2011"},{"issue":"3","key":"10.1016\/B978-0-12-385510-7.00006-0_bb0185","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","article-title":"Proving liveness properties of concurrent programs","volume":"4","author":"Owicki","year":"1982","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0190","series-title":"Temporal Logic: Mathematical Foundations and Computational Aspects","author":"Gabbay","year":"2000"},{"issue":"8","key":"10.1016\/B978-0-12-385510-7.00006-0_bb0195","doi-asserted-by":"crossref","first-page":"1211","DOI":"10.1016\/j.jss.2009.03.102","article-title":"Quality-driven architecture development using architectural tactics","volume":"82","author":"Kim","year":"2009","journal-title":"J. Syst. Software"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0200","doi-asserted-by":"crossref","DOI":"10.1109\/WICSA.2005.29","article-title":"Encapsulating quality attribute knowledge","author":"Bass","year":"2005"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0205","first-page":"9","article-title":"Using models to improve the availability of automotive software architectures","author":"Shelton","year":"2007","journal-title":"ICSE Workshops SEAS '07, IEEE, 20\u201326 May 2007"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0210","first-page":"153","article-title":"Designing software architectures to achieve quality attribute requirements","author":"Bachmann","year":"2005"},{"key":"10.1016\/B978-0-12-385510-7.00006-0_bb0215","doi-asserted-by":"crossref","DOI":"10.4271\/2006-01-0309","article-title":"Effort estimation in model-based software development","author":"Vitkin","year":"2006"}],"container-title":["Advances in Computers"],"original-title":[],"link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780123855107000060?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780123855107000060?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,6,26]],"date-time":"2019-06-26T01:42:58Z","timestamp":1561513378000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780123855107000060"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"references-count":43,"URL":"https:\/\/doi.org\/10.1016\/b978-0-12-385510-7.00006-0","relation":{},"ISSN":["0065-2458"],"issn-type":[{"value":"0065-2458","type":"print"}],"subject":[],"published":{"date-parts":[[2011]]}}}