{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T02:09:31Z","timestamp":1729649371008,"version":"3.28.0"},"reference-count":34,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013,12]]},"DOI":"10.1109\/idt.2013.6727075","type":"proceedings-article","created":{"date-parts":[[2014,1,31]],"date-time":"2014-01-31T23:35:43Z","timestamp":1391211343000},"page":"1-6","source":"Crossref","is-referenced-by-count":4,"title":["Verification of multi decisional reactive agent using SMV model checker"],"prefix":"10.1109","author":[{"given":"Abdelhay","family":"Haqiq","sequence":"first","affiliation":[]},{"given":"Bouchaib","family":"Bounabat","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","first-page":"544","article-title":"Verification of protocol design using uML-SMV","author":"prashanth","year":"2009","journal-title":"World Academy of Science Engineering and Technology"},{"key":"17","first-page":"90","article-title":"Implementing statecharts in pROMELA\/SPIN","author":"mikk","year":"1998","journal-title":"Proceedings. 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques"},{"key":"18","article-title":"UPAAL a tool suite for automatic verification of real-time systems","author":"bengtsson","year":"1995","journal-title":"Proccedings of the 4th DIMACS Workshop on Verification and Control of Hybrid Systems Lecture Notes in Computer Science"},{"key":"33","first-page":"320","article-title":"Mapping template semantics to sMV","author":"lu","year":"2004","journal-title":"Proceedings of the 19th IEEE International Conference on Automated Software Engineering IEEE Computer Society"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.7763\/LNSE.2013.V1.50"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-011-0147-2"},{"journal-title":"NuSMV ITC-Irst","year":"2010","author":"cavada","key":"16"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806850"},{"journal-title":"Symbolic Model Checking An Approach to the State Explosion Problem","year":"1992","author":"mcmillan","key":"14"},{"key":"11","article-title":"Temporal logic for real time systems","author":"ostroff","year":"1989","journal-title":"Advanced Software Development Series"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1145\/1592761.1592781"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.04.008"},{"key":"20","article-title":"Formal verification of embedded software based on software compliance properties and explicit use of time","volume":"5","author":"popovic","year":"2011","journal-title":"International Journal of Computers"},{"journal-title":"A Formal Method for Modeling Verification and Synthesis of Embedded Reactive Systems","year":"2011","author":"caldas","key":"22"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1109\/ARES.2008.194"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1109\/CSSE.2008.976"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1109\/ICCMS.2010.125"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-009-0103-6"},{"key":"27","doi-asserted-by":"crossref","first-page":"289","DOI":"10.3233\/FI-2009-0103","article-title":"A new approach to model checking of uML state machines","volume":"93","author":"niewiadomski","year":"2009","journal-title":"Fundamenta Informaticae"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1109\/SSIRI-C.2010.11"},{"key":"29","article-title":"Modular translation of statecharts to sMV","author":"clarke","year":"2000","journal-title":"Technical Report CMU-CS-00-XXX"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/FSCS.1990.89597"},{"journal-title":"Synchronous Programming of Reactive Systems","year":"2010","author":"halbwachs","key":"2"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/5.97299"},{"journal-title":"Modeling and Verification Using UML Statecharts A Working Guide to Reactive System Design Runtime Monitoring and Execution-Based Model Checking","year":"2006","author":"drusinsky","key":"1"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.2316\/Journal.205.2005.2.205-4136"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46693-2_15"},{"key":"32","first-page":"498","article-title":"Model checking large software specifications software engineering","volume":"24","author":"chan","year":"1998","journal-title":"IEEE Transactions on"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34281-3_21"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2920-7"},{"key":"31","first-page":"255","article-title":"S2N: Model transformation from sPIN to nuSMV in model checking software","author":"jiang","year":"2012","journal-title":"Springer Berlin Heidelberg"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/IAT.2006.105"},{"key":"8","first-page":"50","article-title":"Wireless sensor network simulation of the energy consumption by a multiagents system","volume":"25","author":"romadi","year":"2011","journal-title":"Journal of Theoretical and Applied Information Technology"}],"event":{"name":"2013 Design and Test Symposium (IDT)","start":{"date-parts":[[2013,12,16]]},"location":"Marrakesh, Morocco","end":{"date-parts":[[2013,12,18]]}},"container-title":["2013 8th IEEE Design and Test Symposium"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6717187\/6727071\/06727075.pdf?arnumber=6727075","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,14]],"date-time":"2020-08-14T23:28:27Z","timestamp":1597447707000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6727075\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12]]},"references-count":34,"URL":"https:\/\/doi.org\/10.1109\/idt.2013.6727075","relation":{},"subject":[],"published":{"date-parts":[[2013,12]]}}}