{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:57:42Z","timestamp":1762459062151,"version":"build-2065373602"},"reference-count":37,"publisher":"Elsevier BV","issue":"7","license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["IFAC Proceedings Volumes"],"published-print":{"date-parts":[[2012]]},"DOI":"10.3182\/20120523-3-cz-3015.00028","type":"journal-article","created":{"date-parts":[[2013,2,21]],"date-time":"2013-02-21T18:53:20Z","timestamp":1361472800000},"page":"134-139","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":15,"title":["Hardware Behavioural Modelling, Verification and Synthesis with UML 2.x Activity Diagrams"],"prefix":"10.3182","volume":"45","author":[{"given":"Michal","family":"Grobelny","sequence":"first","affiliation":[]},{"given":"Iwona","family":"Grobelna","sequence":"additional","affiliation":[]},{"given":"Marian","family":"Adamski","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.3182\/20120523-3-CZ-3015.00028_bib1","first-page":"53","article-title":"A rigorous design methodology for reprogrammable logic controllers","author":"Adamski","year":"2001","journal-title":"Proceedings of IFAC Workshop on Discrete Event Systems Design"},{"year":"2011","key":"10.3182\/20120523-3-CZ-3015.00028_bib2"},{"year":"2005","key":"10.3182\/20120523-3-CZ-3015.00028_bib3"},{"unstructured":"Altova GmbH homepage (2011). http:\/\/www.altova.com","key":"10.3182\/20120523-3-CZ-3015.00028_bib4"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib5","first-page":"308","article-title":"Modelling automation systems by UML and Petri Nets","author":"Basile","year":"2008","journal-title":"Proceedings of the 9th International Workshop on Discreet Event Systems"},{"year":"2001","author":"Ben-Ari","series-title":"Mathematical Logic for Computer Science","key":"10.3182\/20120523-3-CZ-3015.00028_bib6"},{"unstructured":"Cavada R. et al. (2010). NuSMV 2.5 user manual. http:\/\/nusmv.fbk.eu\/NuSMV\/userman\/v25\/nusmv.pdf","key":"10.3182\/20120523-3-CZ-3015.00028_bib7"},{"issue":"4","key":"10.3182\/20120523-3-CZ-3015.00028_bib8","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","article-title":"Formal methods: state of the art and future directions","volume":"Volume 28","author":"Clarke","year":"1996","journal-title":"ACM Computing Surveys"},{"year":"1999","author":"Clarke","series-title":"Model checking.","key":"10.3182\/20120523-3-CZ-3015.00028_bib9"},{"year":"1992","author":"David","series-title":"Petri Nets & Grafcet: Tools for modelling discrete event systems.","key":"10.3182\/20120523-3-CZ-3015.00028_bib10"},{"year":"2010","author":"David","series-title":"Discrete, Continuous, and Hybrid Petri Nets.","key":"10.3182\/20120523-3-CZ-3015.00028_bib11"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib12","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/978-3-540-69850-0_2","article-title":"The beginning of model checking: a personal perspective","volume":"Volume 5000","author":"Emerson","year":"2008","journal-title":"Lecture Notes in Computer Scienc"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib13","first-page":"93","article-title":"A Comparison of Petri Net and Activity Diagram Variants","author":"Eshuis","year":"2001","journal-title":"Proc. of 2nd Int. Coll. on Petri Net Technologies for Modelling Communication Based System"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib14","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/978-3-540-69850-0_8","article-title":"Fifteen years of formal property verification in Intel","volume":"Volume 5000","author":"Fix","year":"2008","journal-title":"Lecture Notes in Computer Science"},{"year":"2009","author":"Gajski","series-title":"Embedded System Design. Modeling, Synthesis and Verification.","key":"10.3182\/20120523-3-CZ-3015.00028_bib15"},{"year":"2003","author":"Girault","series-title":"Petri Nets for Systems Engineering. A Guide to Modelling, Verification and Applications","key":"10.3182\/20120523-3-CZ-3015.00028_bib16"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib17","series-title":"The Embedded Systems Handbook,.","article-title":"Modeling Formalisms for Embedded System Design","author":"Gomes","year":"2005"},{"issue":"nr 2","key":"10.3182\/20120523-3-CZ-3015.00028_bib18","first-page":"45","article-title":"Gaps in design and tests of dependable embedded systems","volume":"Volume 2010","author":"Grobelna","year":"2010","journal-title":"Methods of Applied Informatics of Polish Academy of Sciences"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib19","first-page":"607","article-title":"Petri Nets and activity diagrams in logic controller specification -transformation and verification","author":"Grobelna","year":"2010","journal-title":"Mixed Design of Integrated Circuits and Systems (MIXDES), Proceedings of the 17th International Conference"},{"issue":"8","key":"10.3182\/20120523-3-CZ-3015.00028_bib20","first-page":"942","article-title":"Rule-based representation of Control Interpreted Petri Nets for synthesis and verification purposes","volume":"Volume 57","author":"Grobelna","year":"2011","journal-title":"Measurement Automation and Monitoring"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib21","first-page":"621","article-title":"Model Checking of Control Interpreted Petri Nets","author":"Grobelna","year":"2011","journal-title":"Mixed Design of Integrated Circuits and Systems (MIXDES), Proceedings of the 17th International Conference"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib22","first-page":"433","article-title":"A short comparison between UML Activity Diagrams and Petri Nets in hardware behavioural modelling","volume":"Volume 25","author":"Grobelny","year":"2008","journal-title":"Proceedings of X International PHD Workshop - OWD 2008, Conference Archives PTETiS"},{"issue":"10","key":"10.3182\/20120523-3-CZ-3015.00028_bib23","first-page":"1154","article-title":"UML Activity Diagrams and Petri Nets in binary control systems \u2013 from transformation to verification","volume":"Volume 56","author":"Grobelny","year":"2010","journal-title":"Measurement Automation and Monitoring"},{"year":"2004","author":"Huth","series-title":"Logic in Computer Science. Modelling and Reasoning about Systems.","key":"10.3182\/20120523-3-CZ-3015.00028_bib24"},{"year":"2007","author":"Karatkevich","series-title":"Dynamic Analysis of Petri Net-Based Discrete Systems.","key":"10.3182\/20120523-3-CZ-3015.00028_bib25"},{"year":"1999","author":"Kropf","series-title":"Introduction to Formal Hardware Verification.","key":"10.3182\/20120523-3-CZ-3015.00028_bib26"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib27","first-page":"174","article-title":"Sometime is sometimes not never, On the Temporal Logic of Programs","author":"Lamport","year":"1980","journal-title":"Proceedings of the Seventh ACM Symposium on Principles of Programming Languages"},{"unstructured":"Object Management Group homepage (2011). http:\/\/www.omg.org.","key":"10.3182\/20120523-3-CZ-3015.00028_bib28"},{"unstructured":"Petri Net Markup Language (PNML) homepage (2011). http:\/\/www.pnml.org\/","key":"10.3182\/20120523-3-CZ-3015.00028_bib29"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-45319-9_1","article-title":"Branching vs. Linear Time: Final Showdown","volume":"Volume 2031","author":"Rice","year":"2001","journal-title":"Lecture Notes in Computer Science"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib31","doi-asserted-by":"crossref","first-page":"832","DOI":"10.1109\/DATE.2005.320","article-title":"UML 2.0 Overview and Perspectives in SoC Design","author":"Schattkowsky","year":"2005","journal-title":"Proceedings of the Design, Automation and Test in Europe Conference and Exhibition"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib32","first-page":"191","article-title":"Intuitive Mapping of UML 2 Activity Diagrams into Fundamental Modeling Concept Petri Net Diagrams and Colored Petri Nets","author":"Staines","year":"2008","journal-title":"15th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib33","series-title":"Design of Digital Systems and Devices.","article-title":"PeNLogic \u2013 System for Concurrent Logic Controllers Design","author":"Wegrzyn","year":"2011"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib34","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1109\/FPL.2010.74","article-title":"Generation of Deterministic MCU\/FPGA Hybrid Systems from UML Activities","author":"Willenberg","year":"2010","journal-title":"Proceedings of International Conference on Field Programmable Logic and Applications (FPL)"},{"unstructured":"WoPeD homepage (2011). http:\/\/www.woped.org","key":"10.3182\/20120523-3-CZ-3015.00028_bib35"},{"unstructured":"XML Metadata Interchange (XMI\u00ae) homepage (2011). http:\/\/www.omg.org\/spec\/XMI\/","key":"10.3182\/20120523-3-CZ-3015.00028_bib36"},{"key":"10.3182\/20120523-3-CZ-3015.00028_bib37","first-page":"193","article-title":"Workflow Process Definition and Their Applications in e-Commerce","author":"Yen-Liang","year":"2000","journal-title":"Proceedings of the 2000 International Conference on Microelectronic Systems Education"}],"container-title":["IFAC Proceedings Volumes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1474667015350771?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1474667015350771?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T10:56:09Z","timestamp":1761476169000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1474667015350771"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"references-count":37,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2012]]}},"alternative-id":["S1474667015350771"],"URL":"https:\/\/doi.org\/10.3182\/20120523-3-cz-3015.00028","relation":{},"ISSN":["1474-6670"],"issn-type":[{"type":"print","value":"1474-6670"}],"subject":[],"published":{"date-parts":[[2012]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Hardware Behavioural Modelling, Verification and Synthesis with UML 2.x Activity Diagrams","name":"articletitle","label":"Article Title"},{"value":"IFAC Proceedings Volumes","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.3182\/20120523-3-CZ-3015.00028","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2012 IFAC. Published by Elsevier Ltd. All rights reserved.","name":"copyright","label":"Copyright"}]}}