{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T08:42:26Z","timestamp":1649148146628},"reference-count":13,"publisher":"World Scientific Pub Co Pte Lt","issue":"06","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J CIRCUIT SYST COMP"],"published-print":{"date-parts":[[2007,12]]},"abstract":"<jats:p> In this paper, we propose to integrate an embedding of Property Specification Language (PSL) in Abstract State Machines Language (AsmL) with a top\u2013down design for verification approach in order to enable the model checking of large systems at the early stages of the design process. We provide a complete embedding of PSL in the ASM language AsmL, which allows us to integrate PSL properties as a part of the design. For verification, we propose a technique based on the AsmL tool that translates the code containing both the design and the properties into a finite state machine (FSM) representation. We use the generated FSM to run model checking on an external tool, here SMV. Our approach takes advantage of the AsmL language capabilities to model designs at the system level as well as from the power of the AsmL tool in generating both C# code and FSMs from AsmL models. We applied our approach on the PCI-X bus standard, which AsmL model was constructed from the informal standard specifications and a subsequent UML model. Experimental results on the PCI-X bus case study showed a superiority of our approach to conventional verification. <\/jats:p>","DOI":"10.1142\/s0218126607004052","type":"journal-article","created":{"date-parts":[[2008,5,21]],"date-time":"2008-05-21T11:00:28Z","timestamp":1211367628000},"page":"859-881","source":"Crossref","is-referenced-by-count":2,"title":["A DESIGN FOR VERIFICATION APPROACH USING AN EMBEDDING OF PSL IN AsmL"],"prefix":"10.1142","volume":"16","author":[{"given":"AMJAD","family":"GAWANMEH","sequence":"first","affiliation":[{"name":"Concordia University, Montreal, Quebec, H3G 1M8, Canada"}]},{"given":"SOFI\u00c8NE","family":"TAHAR","sequence":"additional","affiliation":[{"name":"Concordia University, Montreal, Quebec, H3G 1M8, Canada"}]},{"given":"HAJA","family":"MOINUDEEN","sequence":"additional","affiliation":[{"name":"SiliconPro Inc., Ottawa, Ontario, K2K 2E2, Canada"}]},{"given":"ALI","family":"HABIBI","sequence":"additional","affiliation":[{"name":"MIPS Technologies, Inc., Mountain View, California, 94043, USA"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"reference":[{"key":"rf1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7"},{"key":"rf2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_24"},{"key":"rf6","volume-title":"Languages for Formal Specification and Verification, Forum on Specification and Design Languages","author":"Gawanmeh A.","year":"2004"},{"key":"rf8","doi-asserted-by":"publisher","DOI":"10.1016\/j.sysarc.2007.03.007"},{"key":"rf9","doi-asserted-by":"publisher","DOI":"10.1145\/566171.566190"},{"key":"rf11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_19"},{"key":"rf12","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","author":"Gordon M.","year":"1993"},{"key":"rf13","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-003-0014-5"},{"key":"rf14","volume-title":"Specification and Validation Methods","author":"Gurevich Y.","year":"1995"},{"key":"rf17","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.01.021"},{"key":"rf19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"rf24","unstructured":"K.\u00a0Shimizu, D.\u00a0Dill and A.\u00a0Hu, Formal Methods in Computer-Aided Design, LNCS 1954 (Springer-Verlag, 2000)\u00a0pp. 335\u2013353."},{"key":"rf26","unstructured":"C.\u00a0Wallace, Specification and Validation Methods (Oxford University Press, 1995)\u00a0pp. 131\u2013164."}],"container-title":["Journal of Circuits, Systems and Computers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218126607004052","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T17:56:07Z","timestamp":1565200567000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218126607004052"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12]]},"references-count":13,"journal-issue":{"issue":"06","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[2007,12]]}},"alternative-id":["10.1142\/S0218126607004052"],"URL":"https:\/\/doi.org\/10.1142\/s0218126607004052","relation":{},"ISSN":["0218-1266","1793-6454"],"issn-type":[{"value":"0218-1266","type":"print"},{"value":"1793-6454","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,12]]}}}