{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T16:15:11Z","timestamp":1778256911299,"version":"3.51.4"},"reference-count":41,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,5]]},"DOI":"10.1109\/notere.2011.5957992","type":"proceedings-article","created":{"date-parts":[[2011,7,21]],"date-time":"2011-07-21T11:18:54Z","timestamp":1311247134000},"page":"1-10","source":"Crossref","is-referenced-by-count":54,"title":["AVATAR: A SysML Environment for the Formal Verification of Safety and Security Properties"],"prefix":"10.1109","author":[{"given":"Gabriel","family":"Pedroza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ludovic","family":"Apvrille","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Knorreck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","article-title":"Secure on-board architecture specification","author":"seudie","year":"2010","journal-title":"EVITA Project Tech Rep Deliverable D3 2"},{"key":"ref38","article-title":"Secure on-board protocols specification","author":"schweppe","year":"2010","journal-title":"EVITA Project Tech Rep Deliverable D3 3"},{"key":"ref33","first-page":"342","article-title":"From Secrecy to Authenticity in Security Protocols","volume":"2477","author":"hermenegildo","year":"2002","journal-title":"9th International Static Analysis Symposium (SAS'02) ser Lecture Notes on Computer Science"},{"key":"ref32","article-title":"Proverif automatic cryptographic protocol verifier user manual","year":"2010","journal-title":"CNRS Departement d'Informatique Ecole Normale Superieure Paris Tech Rep"},{"key":"ref31","doi-asserted-by":"crossref","first-page":"363","DOI":"10.3233\/JCS-2009-0339","article-title":"Automatic verification of correspondences for security protocols","volume":"17","author":"blanchet","year":"2009","journal-title":"Journal of Computer Security"},{"key":"ref30","first-page":"281","article-title":"The AVISPA tool for the automated validation of internet security protocols and applications","volume":"3576","author":"armando","year":"2005","journal-title":"Proc CAV 2005 Ser LNCS"},{"key":"ref37","article-title":"On-Board Architecture and Protocols Verification","author":"fuchs","year":"2010","journal-title":"EVITA Project Tech Rep Deliverable D3 2"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.018"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503277"},{"key":"ref34","article-title":"The computational and decisional Diffie-Hellman assumptions in CryptoVerif","author":"blanchet","year":"2010","journal-title":"Workshop on Formal and Computational Cryptography (FCC 2010)"},{"key":"ref10","article-title":"A UML profile for MARTE, beta 2","year":"2008","journal-title":"OMG"},{"key":"ref11","article-title":"Integrando SysML e model checking para v&v de software critico espacial","author":"da silva","year":"2009","journal-title":"Brasilian Symposium on Aeropspace Engineering and Applications Siio Jose dos Campos Sl’"},{"key":"ref40","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/11557432_19","article-title":"Weaving executability into object-oriented meta-languages","volume":"3713","author":"muller","year":"2005","journal-title":"Model Driven Engineering Languages and Systems Ser Lecture Notes in Computer Science"},{"key":"ref12","first-page":"373","article-title":"OMEGA2: A new version of the profile and the tools (regular paper)","author":"ober","year":"2009","journal-title":"UML&AADL'2009?14th IEEE International Conference on Engineering of Complex Computer Systems Potsdam IEEE"},{"key":"ref13","article-title":"Testing solutions with UML\/SysML","author":"hause","year":"2010"},{"key":"ref14","article-title":"TOPCASED 3.4 tutorial – requirement management","author":"audrain","year":"2010"},{"key":"ref15","article-title":"SysML companion","year":"0"},{"key":"ref16","first-page":"93","article-title":"From UML\/SysML to Mat-lab\/Simulink: current state and future perspectives","author":"vanderperren","year":"2006","journal-title":"DATE'06 Proceedings of the conference on Design automation and test in Europe 3001 Leuven"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/49.223870"},{"key":"ref18","article-title":"Formal language for security services base modelling and analysis","volume":"18","author":"trcek","year":"1995","journal-title":"Elsevier J Comput Commun"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/QSIC.2004.1357945"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/ICECS.2006.379694"},{"key":"ref28","article-title":"A framework towards the efficient identification and modelling of security requirements","author":"idrees","year":"2010","journal-title":"Seme Conf sur la Securite des Architectures Reseaux et Systemes d'Information (SAR-SSI 2010)"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.34"},{"key":"ref6","article-title":"TEPE: A SysML language for timed-constrained property modeling and formal verification","author":"knorreck","year":"2010","journal-title":"Proceedings of the UML&Formal Methods Workshop (UML&FM)"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/SCCC.2007.21"},{"key":"ref29","first-page":"18","article-title":"The sh-verification tool","author":"ochsenschlager","year":"2000","journal-title":"Proceedings of the Thirteenth International Florida Artificial Intelligence Research Society Conference"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2006.244110"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2006.1639422"},{"key":"ref2","article-title":"The EVITA european project","year":"0"},{"key":"ref9","first-page":"14","article-title":"Events and constraints: a graphical editor for capturing logic properties of programs","author":"smith","year":"2001","journal-title":"Proceedings of International Symposium on Requirements Engineering"},{"key":"ref1","article-title":"TTool","year":"0","journal-title":"LabSoc"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2004.1314432"},{"key":"ref22","article-title":"Towards formal specification of abstract security properties","volume":"?7695?3102?4","year":"2008","journal-title":"The Third International Conference on Availability Reliability and Security"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.ress.2006.10.003"},{"key":"ref24","first-page":"412","article-title":"UMLsec: Extending UML for secure systems development","author":"j\u00fcirjens","year":"2002","journal-title":"Proc of International Conference on Shape Modeling"},{"key":"ref23","article-title":"A rigorous methodology for security architecture modeling and verification","volume":"978?0?7695?3450?3","author":"ali","year":"2009","journal-title":"Proceedings of the 42nd Hawaii International Conference on System Sciences"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/EASe.2009.16"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/508791.508847"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2005.67"}],"event":{"name":"2011 11th Annual International Conference on New Technologies of Distributed Systems (NOTERE)","location":"Paris, France","start":{"date-parts":[[2011,5,9]]},"end":{"date-parts":[[2011,5,13]]}},"container-title":["2011 11th Annual International Conference on New Technologies of Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5957344\/5957970\/05957992.pdf?arnumber=5957992","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,13]],"date-time":"2019-06-13T01:19:24Z","timestamp":1560388764000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5957992\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5]]},"references-count":41,"URL":"https:\/\/doi.org\/10.1109\/notere.2011.5957992","relation":{},"subject":[],"published":{"date-parts":[[2011,5]]}}}