T. Hitop, I. , I. Tricore, and . Hitex, In http://www.hitex.com/. [5] The Model Driven Engineering Architecture

B. Weyl, M. Wolf, F. Zweers, T. Gendrullis, M. S. Idrees et al., Secure On-board Architecture Specification, 2010.

D. Dolev and A. Yao, On the security of public key protocols. Information Theory, IEEE Transactions on, vol.29, issue.2, pp.198-208, 1983.

G. L. Mayhew, J. Erlichman, K. L. Shirley, and F. Streff, Development of a Functional Specification for an In-Vehicle Safety Advisory and Warning System (IVSAWS), SAE Technical Paper Series
DOI : 10.4271/912864

D. J. Reitz, Automatic vehicle identification technology and applications, 35th IEEE Vehicular Technology Conference, pp.285-291, 1985.
DOI : 10.1109/VTC.1985.1623367

L. L. Saunders, Automated transit technology development a key to the future, 30th IEEE Vehicular Technology Conference, pp.442-447, 1980.
DOI : 10.1109/VTC.1980.1622849

A. Fuchs, S. Gürgens, G. Pedroza, and L. Apvrille, On-Board Architecture and Protocols Attack Analysis, 2010.

A. Fuchs, S. Gürgens, L. Apvrille, and G. Pedroza, On-Board Architecture and Protocols Verification, 2010.

A. Ruddle, D. Ward, B. Weyl, S. Idrees, Y. Roudier et al., Security requirements for automotive on-board networks based on dark-side scenarios, 2009.

M. Abadi and B. Blanchet, Analyzing security protocols with secrecy types and logic programs, Journal of the ACM, vol.52, issue.1, pp.102-146, 2005.
DOI : 10.1145/1044731.1044735

M. Abadi and A. D. Gordon, A calculus for cryptographic protocols, Proceedings of the 4th ACM conference on Computer and communications security , CCS '97, pp.36-47, 1997.
DOI : 10.1145/266420.266432

J. Abrial, The B-book: assigning programs to meanings, 1996.
DOI : 10.1017/CBO9780511624162

D. Achim and . Brucker, The Isabelle/HOL-OCL environment, 2012.

F. M. Adib and H. M. Hajj, VSpyware: Spyware in VANETs, Local Computer Networks (LCN), 2010 IEEE 35th Conference on, pp.621-624, 2010.

Z. Ahmadian, S. Salimi, and A. Salahi, New attacks on UMTS network access, 2009 Wireless Telecommunications Symposium, pp.1-6, 2009.
DOI : 10.1109/WTS.2009.5068979

M. Albert, J. Cabot, C. Gómez, and V. Pelechano, Automatic generation of basic behavior schemas from UML class diagrams. Software and Systems Modeling, pp.47-67, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00540822

Y. Ali, S. El-kassas, and M. Mahmoud, A rigorous methodology for security architecture modeling and verification, Proceedings of the 4th annual workshop on Cyber security and informaiton intelligence research developing strategies to meet the cyber security and information intelligence challenges ahead, CSIIRW '08, pp.1-10, 2009.
DOI : 10.1145/1413140.1413155

A. I. Alrabady and S. M. Mahmud, Analysis of attacks against the security of keylessentry systems for vehicles and suggestions for improved designs. Vehicular Technology, IEEE Transactions on, vol.54, issue.1, pp.41-50, 2005.

R. Alur, C. Courcoubetis, and D. Dill, Model-checking for real-time systems, Logic in Computer Science LICS '90, Proceedings., Fifth Annual IEEE Symposium on, pp.414-425, 1990.

R. Alur, . Dill, and L. David, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

A. Fuchs, S. Gürgens, and C. Rudolph, A Formal Notion of Trust ??? Enabling Reasoning about Security Properties, Trust Management IV: 4th IFIP WG 11.11 International Conference, IFIPTM 2010 Proceedings, pp.200-215, 2010.
DOI : 10.1007/978-3-642-13446-3_14
URL : https://hal.archives-ouvertes.fr/hal-01061328

L. Apvrille, J. Courtiat, C. Lohr, and P. De-saqui-sannes, TURTLE: a real-time UML profile supported by a formal validation toolkit. Software Engineering, IEEE Transactions on, issue.7, p.30, 2004.

L. Apvrille, W. Muhammad, R. Ameur-boulifa, S. Coudert, and R. Pacalet, A UML-based Environment for System Design Space Exploration, 2006 13th IEEE International Conference on Electronics, Circuits and Systems, 2006.
DOI : 10.1109/ICECS.2006.379694
URL : https://hal.archives-ouvertes.fr/hal-00525101

A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna et al., The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, Computer Aided Verification, pp.135-165, 2005.
DOI : 10.1007/11513988_27
URL : https://hal.archives-ouvertes.fr/inria-00000408

A. Company, The Artisan Studio

P. Autosar-development, Automotive Open System Architecture

B. Blanchet, From Secrecy to Authenticity in Security Protocols, 9th International Static Analysis Symposium (SAS'02), 2002.
DOI : 10.1007/3-540-45789-5_25

B. Blanchet, ProVerif Automatic Cryptographic Protocol Verifier User Manual, 2010.
DOI : 10.1109/csfw.2001.930138
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.5150

M. Backes, C. Hritcu, and M. Maffei, Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus, 2008 21st IEEE Computer Security Foundations Symposium, pp.195-209, 2008.
DOI : 10.1109/CSF.2008.26

G. Barthe, D. Naumann, and T. Rezk, Deriving an information flow checker and certifying compiler for Java, 2006 IEEE Symposium on Security and Privacy (S&P'06), pp.13-242, 2006.
DOI : 10.1109/SP.2006.13

B. Beckert, T. Hoare, R. Hahnle, D. R. Smith, C. Green et al., Intelligent Systems and Formal Methods in Software Engineering, IEEE Intelligent Systems, vol.21, issue.6, pp.71-81, 2006.
DOI : 10.1109/MIS.2006.117

J. A. Bergstra, Handbook of Process Algebra, 2001.

D. Bjørner and M. C. Henson, Logics of Specification Languages. Monographs in Theoretical Computer Science, 2008.

B. Blanchet and A. Podelski, Verification of cryptographic protocols: tagging enforces termination, Foundations of Software Science and Computation Structures, pp.67-90, 2005.
DOI : 10.1016/j.tcs.2004.10.018

J. J. Blum, A. Neiswender, and A. Eskandarian, Denial of Service Attacks on Inter-Vehicle Communication Networks, 2008 11th International IEEE Conference on Intelligent Transportation Systems, 2008.
DOI : 10.1109/ITSC.2008.4732612

S. C. Bono, M. Green, A. Stubblefield, A. Juels, R. et al., Security analysis of a cryptographically-enabled RFID device, Proceedings of the 14th conference on USENIX Security Symposium SSYM'05, 2005.

R. Bouroulet, H. Klaudel, and E. Pelz, A semantics of security protocol language (SPL) using a class of composable high-level Petri nets, Proceedings. Fourth International Conference on Application of Concurrency to System Design, 2004. ACSD 2004., pp.99-108, 2004.
DOI : 10.1109/CSD.2004.1309120

G. Brasche, C. Rokitansky, and C. Wietfeld, Communication architecture and performance analysis of protocols for RTT infrastructure networks and vehicleroadside communications, Vehicular Technology Conference, pp.384-390, 1994.

R. R. Brooks, S. Sander, J. Deng, and J. Taiber, Automotive system security, Proceedings of the 4th annual workshop on Cyber security and informaiton intelligence research developing strategies to meet the cyber security and information intelligence challenges ahead, CSIIRW '08, pp.1-26, 2008.
DOI : 10.1145/1413140.1413170

G. Brown, B. H. Cheng, H. Goldsby, and J. Zhang, Goaloriented specification of adaptation requirements engineering in adaptive systems, Proceedings of the 2006 international workshop on Self-adaptation and self-managing systems, SEAMS '06, pp.23-29, 2006.

B. Schneier, Attack Trees. Dr. Dobb's, Journal, 1999.

B. Blanchet, Automatic verification of correspondences for security protocols*, Journal of Computer Security, vol.17, issue.4, pp.363-434, 2009.
DOI : 10.3233/JCS-2009-0339

C. Mellon, The SMV model checker

L. Cheng and Y. Zhang, Model checking security policy model using both UML static and dynamic diagrams, Proceedings of the 4th international conference on Security of information and networks, SIN '11, pp.159-166, 2011.
DOI : 10.1145/2070425.2070451

L. Compagna, U. Flegel, and V. Lotz, Towards Validating Security Protocol Deployment in the Wild, 2009 33rd Annual IEEE International Computer Software and Applications Conference, 2009.
DOI : 10.1109/COMPSAC.2009.172

C. Constant, T. Jeron, H. Marchand, and V. Rusu, Integrating formal verification and conformance testing for reactive systems, IEEE Transactions on Software Engineering, vol.33, issue.8, pp.558-574, 2007.
DOI : 10.1109/TSE.2007.70707
URL : https://hal.archives-ouvertes.fr/inria-00422904

J. Courtiat, R. C. De-oliveira, and L. Andriantsiferana, Specification and validation of multimedia protocols using RT-LOTOS, Proceedings of the Fifth IEEE Computer Society Workshop on Future Trends of Distributed Computing Systems, pp.354-362, 1995.
DOI : 10.1109/FTDCS.1995.525004

F. Cuppens, N. Cuppens-boulahia, and T. Ramard, Availability enforcement by obligations and aspects identification, First International Conference on Availability, Reliability and Security (ARES'06), 2006.
DOI : 10.1109/ARES.2006.36

F. Cuppens and A. Miege, Modelling contexts in the Or-BAC model, 19th Annual Computer Security Applications Conference, 2003. Proceedings., pp.416-425, 2003.
DOI : 10.1109/CSAC.2003.1254346

L. Cysneiros, . Marcio, J. C. Do-prado-leite, and . Sampaio, Non-functional requirements, Proceedings of the 24th international conference on Software engineering , ICSE '02, pp.699-700, 2002.
DOI : 10.1145/581339.581452

D. Knorreck, L. Apvrille, and P. , TEPE, Proceedings of the UML&Formal Methods Workshop (UML&FM), 2010.
DOI : 10.1145/1921532.1921556
URL : https://hal.archives-ouvertes.fr/hal-00667841

B. David, D. A. Johnson, and . Maltz, Dynamic source routing in ad hoc wireless networks, Mobile Computing, pp.153-181, 1996.

F. Davoli, A. Giordano, and S. Zappatore, Architecture and protocol design for a car-to-infrastructure packet radio network, [Proceedings] GLOBECOM '90: IEEE Global Telecommunications Conference and Exhibition, pp.1579-1585, 1990.
DOI : 10.1109/GLOCOM.1990.116756

H. Dhall, D. Dhall, S. Batra, and P. Rani, Implementation of IPSec Protocol, 2012 Second International Conference on Advanced Computing & Communication Technologies, p.2012
DOI : 10.1109/ACCT.2012.64

D. Xu, M. Tu, M. Sanford, L. Thomas, D. Woodraska et al., Automated Security Test Generation with Formal Threat Models. Dependable and Secure Computing, IEEE Transactions on, vol.9, issue.4, pp.526-540, 2012.

R. Dixit and L. Rafaelli, Radar requirements and architecture trades for automotive applications, 1997 IEEE MTT-S International Microwave Symposium Digest, pp.1253-1256, 1997.
DOI : 10.1109/MWSYM.1997.596554

C. Dixon and M. Fisher, Resolution-based proof for multi-modal temporal logics of knowledge, Proceedings Seventh International Workshop on Temporal Representation and Reasoning. TIME 2000, pp.69-78, 2000.
DOI : 10.1109/TIME.2000.856587

C. Dixon, M. F. Gago, M. Fisher, and W. Van-der-hoek, Using temporal logics of knowledge in the formal verification of security protocols, Proceedings. 11th International Symposium on Temporal Representation and Reasoning, 2004. TIME 2004., pp.148-151, 2004.
DOI : 10.1109/TIME.2004.1314432

M. Drouineaud, M. Bortin, P. Torrini, and K. Sohr, A first step towards formal verification of security policy properties for RBAC, Fourth International Conference onQuality Software, 2004. QSIC 2004. Proceedings., pp.60-67, 2004.
DOI : 10.1109/QSIC.2004.1357945

J. Dubreuil, G. Bouffard, J. Lanet, and J. Cartigny, Type Classification against Fault Enabled Mutant in Java Based Smart Card, 2012 Seventh International Conference on Availability, Reliability and Security, pp.551-556
DOI : 10.1109/ARES.2012.24
URL : https://hal.archives-ouvertes.fr/hal-00937292

E. Mendelson, Introduction to Mathematical Logic, 2001.
DOI : 10.1007/978-1-4615-7288-6

E. Project, European Commission FP7, 2008.

M. Faezipour, . Nourani, . Mehrdad, A. Saeed, and S. Addepalli, Progress and challenges in intelligent vehicle area networks, Communications of the ACM, vol.55, issue.2, pp.90-100, 2012.
DOI : 10.1145/2076450.2076470

F. Wang, Formal verification of timed systems: a survey and perspective, Proceedings of the IEEE, pp.1283-1305, 2004.

W. F. Fincham and C. Phillips, An asynchronous two-wire message bus for automotives, Vehicle Networks for Multiplexing and Data Communication, pp.8-9, 1988.

B. Fontan, L. Apvrille, P. De-saqui-sannes, and J. Courtiat, Real-Time and Embedded System Verification Based on Formal Requirements, 2006 International Symposium on Industrial Embedded Systems, pp.1-10, 2006.
DOI : 10.1109/IES.2006.357467

A. P. Fournaris, Hardware Module Design for Ensuring Trust, 2010 IEEE Computer Society Annual Symposium on VLSI, pp.155-160, 2010.
DOI : 10.1109/ISVLSI.2010.80

R. France, I. Ray, G. Georg, and S. Ghosh, Aspect-oriented approach to early design modelling, IEE Proceedings - Software, vol.151, issue.4, pp.173-185, 2004.
DOI : 10.1049/ip-sen:20040920

F. Stumpf, C. Meves, B. Weyl, and M. Wolf, A Security Architecture for Multipurpose ECUs in Vehicles, 25. VDI/VW- Gemeinschaftstagung: Automotive Security, 2009.

A. Fuxman, L. Liu, J. Mylopoulos, M. Pistore, M. Roveri et al., Specifying and analyzing early requirements in Tropos, Requirements Engineering, vol.9, issue.2
DOI : 10.1007/s00766-004-0191-7

G. Pedroza and L. Apvrille, LLD Modeling, Verification and Automatic C-Code Generation, 2012.

G. Georg, K. Anastasakis, B. Bordbar, S. H. Houmb, I. Ray et al., Verification and Trade-Off Analysis of Security Properties in UML System Models. Software Engineering, IEEE Transactions on, vol.36, issue.3, pp.338-356, 2010.

G. Behrmann, A. David, and K. G. Larsen, A Tutorial on Uppaal, International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004. Revised Lectures, pp.200-237
DOI : 10.1007/978-3-540-30080-9_7

M. Gerlach, Trust for Vehicular Applications, Eighth International Symposium on Autonomous Decentralized Systems (ISADS'07), pp.295-304, 2007.
DOI : 10.1109/ISADS.2007.76

P. Giorgini, F. Massacci, and N. Zannone, Foundations of Security Analysis and Design III. chapter Security and trust requirements engineering, pp.237-272, 2005.

M. Glinz, On Non-Functional Requirements, 15th IEEE International Requirements Engineering Conference (RE 2007), pp.21-26, 2007.
DOI : 10.1109/RE.2007.45

A. Gotsman, F. Massacci, and M. Pistore, Towards an Independent Semantics and Verification Technology for the HLPSL Specification Language, Proceedings of the Second Workshop on Automated Reasoning for Security Protocol Analysis, pp.59-77, 2005.
DOI : 10.1016/j.entcs.2005.06.004

H. Schweppe, M. S. Idrees, Y. Roudier, B. Weyl, R. Khayari et al., Secure on-board protocols specification, 2010.

K. Haataja and P. Toivanen, Two practical man-in-the-middle attacks on Bluetooth secure simple pairing and countermeasures, IEEE Transactions on Wireless Communications, vol.9, issue.1, pp.384-392, 2010.
DOI : 10.1109/TWC.2010.01.090935

H. Yang, H. Luo, F. Ye, S. Lu, and L. Zhang, Security in mobile ad hoc networks: challenges and solutions, IEEE Wireless Communications, vol.11, issue.1, pp.38-47, 2004.
DOI : 10.1109/MWC.2004.1269716

H. Liao, J. Jiang, and Y. Zhang, A Study of Automatic Code Generation, 2010 International Conference on Computational and Information Sciences, pp.689-691, 2010.
DOI : 10.1109/ICCIS.2010.171

R. Hassan, S. Bohner, S. El-kassas, and M. Hinchey, Integrating Formal Analysis and Design to Preserve Security Properties, System Sciences, 2009.

X. He, H. Yu, T. Shi, J. Ding, and Y. Deng, Formally analyzing software architectural specifications using SAM, Journal of Systems and Software, vol.71, issue.1-2, pp.11-29, 2004.
DOI : 10.1016/S0164-1212(02)00087-0

H. Kwak and I. Lee, Process algebraic approach to the parametric analysis of object scheduling in real-time systems, Object-Oriented Real-Time Dependable Systems WORDS 1999 Fall. Proceedings. Fifth International Workshop on, pp.131-138, 1999.

G. Heiser, T. Murray, and G. Klein, It's Time for Trustworthy Systems, IEEE Security & Privacy Magazine, vol.10, issue.2, pp.67-70
DOI : 10.1109/MSP.2012.41

S. Hussain, H. Erwin, and P. Dunne, Threat modeling using formal methods: A new approach to develop secure web applications, 2011 7th International Conference on Emerging Technologies, pp.1-5, 2011.
DOI : 10.1109/ICET.2011.6048492

T. Hyo, . Jung, and L. Gil-haeng, A systematic software development process for non-functional requirements, Information and Communication Technology Convergence (ICTC), 2010 International Conference on, pp.431-436, 2010.

. Company, The Rhapsody tool

J. Bengtsson and W. Yi, Timed Automata: Semantics, Algorithms and Tools. In Lecture Notes on Concurrency and Petri Nets, LNCS, vol.3098, 2004.

J. Kim, C. Lim, and T. Han, A Model-Based Design Tool of Automotive Software Architecture, 2010 IEEE 34th Annual Computer Software and Applications Conference, pp.541-542, 2010.
DOI : 10.1109/COMPSAC.2010.60

J. Yu and B. M. Wilamowski, Recent advances in in-vehicle embedded systems, IECON 2011 -37th Annual Conference on IEEE Industrial Electronics Society, pp.4623-4625, 2011.

E. John, J. D. Hopcroft, and . Ullman, Introduction to Automata Theory, Languages and Computation, 1979.

J. Jürjens, UMLsec: Extending UML for Secure Systems Development, Proceedings of the 5th International Conference on The Unified Modeling Language, UML '02, pp.412-425, 2002.
DOI : 10.1007/3-540-45800-X_32

J. Jürjens, Sound methods and effective tools for model-based security engineering with UML, Proceedings of the 27th international conference on Software engineering, ICSE '05, pp.322-331, 2005.

S. Kandl, R. Kirner, and P. Puschner, Automated Formal Verification and Testing of C Programs for Embedded Systems, 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC'07), pp.373-381, 2007.
DOI : 10.1109/ISORC.2007.22

A. Koltuksuz, B. Kulahcioglu, and M. Ozkan, Utilization of Timed Automata as a Verification Tool for Security Protocols, 2010 Fourth International Conference on Secure Software Integration and Reliability Improvement Companion, pp.86-93, 2010.
DOI : 10.1109/SSIRI-C.2010.27

S. Konrad, B. H. Cheng, and L. A. Campbell, Object analysis patterns for embedded systems, IEEE Transactions on Software Engineering, vol.30, issue.12, pp.970-992, 2004.
DOI : 10.1109/TSE.2004.102

P. Koopman, Critical embedded automotive networks. Micro, IEEE, vol.22, issue.4, pp.14-18, 2002.

P. Koopman, Embedded system security, Computer, vol.37, issue.7, pp.95-97, 2004.
DOI : 10.1109/MC.2004.52

H. Kopetz, The Complexity Challenge in Embedded System Design, 2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC), pp.3-12, 2008.
DOI : 10.1109/ISORC.2008.14

K. Koscher, A. Czeskis, . Roesner, . Franziska, . Patel et al., Experimental Security Analysis of a Modern Automobile, 2010 IEEE Symposium on Security and Privacy, pp.447-462, 2010.
DOI : 10.1109/SP.2010.34

L. Apvrille and A. Becoulet, Prototyping an Embedded Automotive System from its UML/SysML Models, ERTSS'2012, 2012.

U. E. Larson, D. K. Nilsson, and E. Jonsson, An approach to specification-based attack detection for in-vehicle networks, 2008 IEEE Intelligent Vehicles Symposium, pp.220-225, 2008.
DOI : 10.1109/IVS.2008.4621263

U. E. Larson, . Nilsson, and K. Dennis, Securing vehicles against cyber attacks on Cyber security and information intelligence research: developing strategies to meet the cyber security and information intelligence challenges ahead, CSIIRW '08, Proceedings of the 4th annual workshop, pp.1-30, 2008.

K. Lemke, C. Paar, and M. Wolf, Embedded Security in Cars, Securing Current and Future Automotive IT Applications, 2006.

L. Mixia, Z. Qiuyu, Y. Dongmei, and Z. Hong, Formal security model research based on Petri-net, Granular Computing, 2005 IEEE International Conference on, pp.575-578, 2005.

T. Lodderstedt, D. A. Basin, and J. Doser, SecureUML: A UML-Based Modeling Language for Model-Driven Security, Proceedings of the 5th International Conference on The Unified Modeling Language, UML '02, pp.426-441, 2002.
DOI : 10.1007/3-540-45800-X_33

G. Lowe, A hierarchy of authentication specifications, Proceedings 10th Computer Security Foundations Workshop, pp.31-43, 1997.
DOI : 10.1109/CSFW.1997.596782

J. Machemie, C. Mazin, J. Lanet, and J. Cartigny, SmartCM a smart card fault injection simulator, 2011 IEEE International Workshop on Information Forensics and Security, pp.1-6, 2011.
DOI : 10.1109/WIFS.2011.6123124
URL : https://hal.archives-ouvertes.fr/hal-00685220

Q. A. Malik, D. Truscan, and J. Lilius, Using UML Models and Formal Verification in Model-Based Testing, 2010 17th IEEE International Conference and Workshops on Engineering of Computer Based Systems, pp.50-56, 2010.
DOI : 10.1109/ECBS.2010.13

F. Massacci, J. Mylopoulos, and N. Zannone, Computer-aided Support for Secure Tropos, Automated Software Engineering, vol.26, issue.10, pp.341-364, 2007.
DOI : 10.1007/s10515-007-0013-5

M. Planck and I. Informatik, The SPASS Theorem Prover

J. Millward, System Architectures for Safety Critical Automotive Applications In Safety Critical Software in Vehicle and Traffic Control, IEE Colloquium on, pp.4-5, 1990.

M. Corporation, Attacks on Mobile and Embedded Systems: Currrent Trends

S. Modersheim and P. Modesti, Verifying SeVeCom using set-based abstraction, 2011 7th International Wireless Communications and Mobile Computing Conference, pp.1164-1169, 2011.
DOI : 10.1109/IWCMC.2011.5982705

N. Moebius, K. Stenzel, and W. Reif, Generating formal specifications for security-critical applications - A model-driven approach, 2009 ICSE Workshop on Software Engineering for Secure Systems, pp.68-74, 2009.
DOI : 10.1109/IWSESS.2009.5068461

S. Mondal and S. Sural, Security Analysis of Temporal-RBAC Using Timed Automata, 2008 The Fourth International Conference on Information Assurance and Security, pp.37-40, 2008.
DOI : 10.1109/IAS.2008.10

S. Morimoto, . Shigematsu, . Shinjiro, Y. Goto, and J. Cheng, Formal verification of security specifications with common criteria, Proceedings of the 2007 ACM symposium on Applied computing , SAC '07, pp.1506-1512, 2007.
DOI : 10.1145/1244002.1244325

M. S. Idrees, Y. Roudier, and L. Apvrille, A Framework Towards the Efficient Identification and Modelling of Security Requirements, 5ème Conf. sur la Sécurité des Architectures Réseaux et Systèmes d'Information (SAR-SSI 2010), 2010.

T. Murata, Petri nets: Properties, analysis and applications, Proceedings of the IEEE, pp.541-580, 1989.
DOI : 10.1109/5.24143

T. Nolte, H. Hansson, and L. L. Bello, Automotive Communications - Past, Current and Future, 2005 IEEE Conference on Emerging Technologies and Factory Automation, pp.8-992, 2005.
DOI : 10.1109/ETFA.2005.1612631

I. Ober and I. Dragomir, OMEGA2: A New Version of the Profile and the Tools, 2010 15th IEEE International Conference on Engineering of Complex Computer Systems, pp.373-378, 2010.
DOI : 10.1109/ICECCS.2010.41

I. Ober and I. Dragomir, OMEGA2: A new version of the profile and the tools (regular paper), UML&AADL'2009 -14th IEEE International Conference on Engineering of Complex Computer Systems, pp.373-378, 2009.

P. Ochsenschläger, J. Repp, and R. Rieke, The SH-Verification Tool, Proc. 13th International Florida Artificial Intelligence Research Society Conference (FLAIRS-2000), pp.18-22, 2000.

P. Ochsenschläger, J. Repp, and R. Rieke, Verification of Cooperating Systems ? An Approach Based on Formal Languages, Proc. 13th International Florida Artificial Intelligence Research Society Conference (FLAIRS-2000), pp.346-350, 2000.

A. Pao, S. Hsiung, C. Lin, T. Tseng, J. Lee et al., VERTAF: an application framework for the design and verification of embedded real-time software. Software Engineering, IEEE Transactions on, vol.30, issue.10, pp.656-674, 2004.

P. Papadimitratos and Z. J. Haas, Secure message transmission in mobile ad hoc networks, Ad Hoc Networks, pp.193-209, 2003.
DOI : 10.1016/S1570-8705(03)00018-0

P. Papadimitratos, On the Road " -Reflections on the security of Vehicular communication systems, Vehicular Electronics and Safety ICVES 2008. IEEE International Conference on, pp.359-363, 2008.

P. Papadimitratos, L. Buttyan, T. Holczer, E. Schoch, J. Freudiger et al., Secure vehicular communication systems: design and architecture, IEEE Communications Magazine, vol.46, issue.11, pp.46100-109, 2008.
DOI : 10.1109/MCOM.2008.4689252
URL : http://arxiv.org/abs/0912.5391

P. Papadimitratos, L. Fortelle, A. Evenssen, K. Brignolo, R. Cosenza et al., Vehicular communication systems: Enabling technologies, applications, and future outlook on intelligent transportation, IEEE Communications Magazine, vol.47, issue.11, pp.4784-95, 2009.
DOI : 10.1109/MCOM.2009.5307471

G. Pedroza, L. Apvrille, and D. Knorreck, AVATAR: A SysML Environment for the Formal Verification of Safety and Security Properties, 2011 11th Annual International Conference on New Technologies of Distributed Systems, pp.1-10, 2011.
DOI : 10.1109/NOTERE.2011.5957992

G. Pedroza, M. S. Idrees, L. Apvrille, and Y. Roudier, A Formal Methodology Applied to Secure Over-the-Air Automotive Applications, 2011 IEEE Vehicular Technology Conference (VTC Fall), 2011.
DOI : 10.1109/VETECF.2011.6093061

C. E. Perkins and E. M. Royer, Ad-hoc on-demand distance vector routing, Mobile Computing Systems and Applications, 1999. Proceedings. WMCSA '99. Second IEEE Workshop on, pp.90-100, 1999.

L. Piètre-cambacédès and M. Bouissou, Beyond Attack Trees: Dynamic Security Modeling with Boolean Logic Driven Markov Processes (BDMP), 2010 European Dependable Computing Conference, pp.199-208, 2010.
DOI : 10.1109/EDCC.2010.32

L. Pirzadeh and E. Jonsson, A Cause and Effect Approach towards Risk Analysis, 2011 Third International Workshop on Security Measurements and Metrics, pp.80-83, 2011.
DOI : 10.1109/Metrisec.2011.20

A. Pretschner, M. Broy, . Kruger, H. Ingolf, and T. Stauner, Software Engineering for Automotive Systems: A Roadmap, Future of Software Engineering (FOSE '07), pp.55-71, 2007.
DOI : 10.1109/FOSE.2007.22

M. Raya and J. Hubaux, The security of vehicular ad hoc networks, Proceedings of the 3rd ACM workshop on Security of ad hoc and sensor networks , SASN '05, pp.11-21, 2005.
DOI : 10.1145/1102219.1102223

R. Milner, Communicating and Mobile Systems, The Pi Calculus, 1999.

M. Rounds and N. Pendgraft, Diversity in Network Attacker Motivation: A Literature Review, 2009 International Conference on Computational Science and Engineering, pp.319-323, 2009.
DOI : 10.1109/CSE.2009.178

R. Jose, F. Harjani, R. , M. , A. Desnitsky et al., A Methodology for the Analysis and Modeling of Security Threats and Attacks for Systems of Embedded Components, Parallel, Distributed and Network-Based Processing (PDP), 2012 20th Euromicro International Conference on, pp.261-268, 2012.

S. Gürgens, P. Ochsenschläger, and C. Rudolph, On a formal framework for security properties Special issue on formal methods, techniques and tools for secure and reliable applications, International Computer Standards & Interface Journal (CSI), 2004.

I. Schaefer and R. Hahnle, Formal Methods in Software Product Line Engineering, Computer, vol.44, issue.2, pp.82-85, 2011.
DOI : 10.1109/MC.2011.47

J. M. Spivey, The Z notation: a reference manual, 1989.

C. Sprenger and D. Basin, Cryptographically-Sound Protocol-Model Abstractions, Logic in Computer Science, 2008. LICS '08. 23rd Annual IEEE Symposium on, pp.3-17, 2008.
DOI : 10.1109/csf.2008.19
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.323.6473

S. Srivastava and A. P. Singh, Testing of embedded system using fault modeling, 2009 International Conference on Emerging Trends in Electronic and Photonic Devices & Systems, pp.177-180, 2009.
DOI : 10.1109/ELECTRO.2009.5441142

A. Stango, N. R. Prasad, and D. M. Kyriazanos, A Threat Analysis Methodology for Security Evaluation and Enhancement Planning, 2009 Third International Conference on Emerging Security Information, Systems and Technologies, pp.262-267, 2009.
DOI : 10.1109/SECURWARE.2009.47

S. Checkoway, D. Mccoy, B. Kantor, D. Anderson, H. Shacham et al., Comprehensive Experimental Analyses of Automotive Attack Surfaces, 20th USENIX conference on Security, 2011.

J. Stern, Why Provable Security Matters?, Proceedings of the 22nd international conference on Theory and applications of cryptographic techniques, EURO- CRYPT'03, pp.449-461, 2003.
DOI : 10.1007/3-540-39200-9_28

H. Stubing, M. Bechler, D. Heussner, T. May, I. Radusch et al., simTD: a car-to-X system architecture for field operational tests, Topics in Automotive Networking]. Communications Magazine, pp.48148-154, 2010.

J. Sun and Y. Fang, Defense against misbehavior in anonymous vehicular ad hoc networks, Ad Hoc Networks Privacy and Security in Wireless Sensor and Ad Hoc Networks, pp.1515-1525, 2009.
DOI : 10.1016/j.adhoc.2009.04.013

N. Thang, . Truong, and T. Katayama, Specification and verification of intercomponent constraints in CTL, Proceedings of the 2005 conference on Specification and verification of component-based systems, SAVCBS '05, 2005.

C. The and . Consortium, car-to-car.org/. [187] The ISO/IEC. The ISO/IEC 15408 standard, 2004.

O. The and . Organization, The SysML language In http://www.omgsysml.org/. [191] The Raytheon Company, GPS OCX technology, 2011.

U. The and . Marte, The MARTE site

T. Gendrullis and M. Wolf, Design, Implementation, and Evaluation of a Vehicular Hardware Security Module, 14th International Conference on Information Security and Cryptology 2011 (ICISC), 2011.

T. Kosch, Local Danger Warning based on Vehicle Ad-hoc Networks, Prototype and Simulation, Proceedings of 1st International Workshop on Intelligent Transportation (WIT), 2004.

I. A. Tndel, J. Jensen, and L. Rstad, Combining Misuse Cases with Attack Trees and Security Activity Models, 2010 International Conference on Availability, Reliability and Security, pp.438-445, 2010.
DOI : 10.1109/ARES.2010.101

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, 2002.

T. Bolognesi and E. Brinksma, Introduction to the ISO specification language LOTOS, Computer Networks and ISDN Systems, vol.14, issue.1, pp.25-59, 1987.
DOI : 10.1016/0169-7552(87)90085-7

. Tu-munchen, The AutoFocus tool

. Ufasoft, The wireless sniffer Ufasoft Snif

T. Vaa, M. Penttinen, and I. Spyropoulou, Intelligent transport systems and effects on road traffic accidents: state of the art, IET Intelligent Transport Systems, vol.1, issue.2, pp.81-88, 2007.
DOI : 10.1049/iet-its:20060081

M. Vetterling, G. Wimmel, and A. Wisspeintner, Secure systems development based on the common criteria: the PalME project, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, SIGSOFT '02/FSE-10, pp.129-138, 2002.

D. Vidakovic and D. Simic, A Novel Approach to Building Secure Systems, The Second International Conference on Availability, Reliability and Security (ARES'07), pp.1074-1084, 2007.
DOI : 10.1109/ARES.2007.11

J. Voelcker, Stalked by satellite - an alarming rise in GPS-enabled harassment, IEEE Spectrum, vol.43, issue.7, pp.4315-4331, 2006.
DOI : 10.1109/MSPEC.2006.1652998

W. Wang, . Zeng, . Qingkai, and A. P. Mathur, A Security Assurance Framework Combining Formal Verification and Security Functional Testing, 2012 12th International Conference on Quality Software, pp.136-139
DOI : 10.1109/QSIC.2012.34

W. Tsai, L. Yu, F. Zhu, and R. Paul, Rapid embedded system testing using verification patterns. Software, IEEE, vol.22, issue.4, pp.68-75, 2005.

R. B. Weld, Communications flow considerations in vehicle navigation and information systems, Conference Record of papers presented at the First Vehicle Navigation and Information Systems Conference (VNIS '89), pp.373-375, 1989.
DOI : 10.1109/VNIS.1989.98795

P. C. Wilson, Electromagnetic compatibility, Telecommunications Energy Conference INTELEC '85. Seventh International, pp.79-85, 1985.
DOI : 10.1016/B978-0-08-097138-4.00008-2

C. Xenakis, D. Apostolopoulou, A. Panou, and I. Stavrakakis, A Qualitative Risk Analysis for the GPRS Technology, 2008 IEEE/IFIP International Conference on Embedded and Ubiquitous Computing, pp.61-68, 2008.
DOI : 10.1109/EUC.2008.123

X. Wu, H. Ling, and Y. Dong, On Modeling and Verifying of Application Protocols of TTCAN in Flight-Control System with UPPAAL, 2009 International Conference on Embedded Software and Systems, pp.572-577, 2009.
DOI : 10.1109/ICESS.2009.27

Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes-drielsma, J. Mantovani et al., A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols, Austrian Computer Society, pp.193-205, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00100219

Y. Roudier, H. Schweppe, and L. Apvrille, Test Specification, 2011.

Y. Roudier, H. Schweppe, L. Apvrille, and G. Pedroza, Test Results, 2012.

Y. Qian and N. Moayeri, Design of Secure and Application-Oriented VANETs, VTC Spring 2008, IEEE Vehicular Technology Conference, pp.2794-2799, 2008.
DOI : 10.1109/VETECS.2008.610

Y. Wang, Z. Jin, and X. Zhao, Practical Defense against WEP and WPA-PSK Attack for WLAN, 2010 International Conference on Computational Intelligence and Software Engineering, pp.1-4, 2010.
DOI : 10.1109/WICOM.2010.5600921

Y. Zhao and D. Ma, Embedded real-time system modeling and analysis using AADL, Networking and Information Technology (ICNIT), 2010 International Conference on, pp.247-251, 2010.