{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T23:34:36Z","timestamp":1775086476587,"version":"3.50.1"},"reference-count":18,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"9","license":[{"start":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T00:00:00Z","timestamp":1630454400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T00:00:00Z","timestamp":1630454400000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T00:00:00Z","timestamp":1630454400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T00:00:00Z","timestamp":1630454400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100006134","name":"Office of Energy Efficiency and Renewable Energy","doi-asserted-by":"publisher","award":["DE-EE0009046"],"award-info":[{"award-number":["DE-EE0009046"]}],"id":[{"id":"10.13039\/100006134","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computer"],"published-print":{"date-parts":[[2021,9]]},"DOI":"10.1109\/mc.2021.3087519","type":"journal-article","created":{"date-parts":[[2021,8,27]],"date-time":"2021-08-27T20:08:24Z","timestamp":1630094904000},"page":"59-71","source":"Crossref","is-referenced-by-count":5,"title":["A Case Study in the Formal Modeling of Safe and Secure Manufacturing Automation"],"prefix":"10.1109","volume":"54","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6960-0181","authenticated-orcid":false,"given":"Matthew","family":"Jablonski","sequence":"first","affiliation":[{"name":"George Mason University, Fairfax, Virginia United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bo","family":"Yu","sequence":"additional","affiliation":[{"name":"George Mason University, Fairfax, Virginia United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriela Felicia","family":"Ciocarlie","sequence":"additional","affiliation":[{"name":"CYMANII, New York City, New York United States"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8280-1551","authenticated-orcid":false,"given":"Paulo","family":"Costa","sequence":"additional","affiliation":[{"name":"George Mason University, Fairfax, Virginia United States"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2011.39"},{"key":"ref11","first-page":"1166","article-title":"Towards a formal semantics for the AADL behavior annex","author":"yang","year":"0","journal-title":"Proc Conf Design Autom Test Europe"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/1566445.1566495"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/PIC.2010.5687484"},{"key":"ref14","author":"procter","year":"2019","journal-title":"The AADL error library"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2658982.2527271"},{"key":"ref16","year":"2019","journal-title":"NuSMV A New Symbolic Model Checker"},{"key":"ref17","year":"2021","journal-title":"Welcome to OSATE"},{"key":"ref18","author":"feiler","year":"2019","journal-title":"The open source aadl tool environment (osate)"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.01.005"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.25365\/thesis.47558"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2008.51"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/SBESC.2011.18"},{"key":"ref8","author":"feiler","year":"2013","journal-title":"Model-Based Engineering with AADL An Introduction to the SAE Architecture Analysis & Design Language"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/ISCIT.2005.1566899"},{"key":"ref2","author":"kroger","year":"2008","journal-title":"Temporal Logic and State Systems"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1201\/9781315216140"},{"key":"ref9","author":"delange","year":"2017","journal-title":"AADL in Practice Become an Expert of Software Architecture Modeling and Analysis"}],"container-title":["Computer"],"original-title":[],"link":[{"URL":"https:\/\/ieeexplore.ieee.org\/ielam\/2\/9524643\/9524644-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/2\/9524643\/09524644.pdf?arnumber=9524644","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,10]],"date-time":"2022-05-10T14:48:30Z","timestamp":1652194110000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9524644\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9]]},"references-count":18,"journal-issue":{"issue":"9"},"URL":"https:\/\/doi.org\/10.1109\/mc.2021.3087519","relation":{},"ISSN":["0018-9162","1558-0814"],"issn-type":[{"value":"0018-9162","type":"print"},{"value":"1558-0814","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,9]]}}}