. L. Chacune-d-'entre-elles, exécution sur lapremì ere sous-trace est classique tandis que sur l'autre elle varie En effet, l'automate de Büchi est initialisé avec l'ensemble desétatsdesétats de l'automate au lieu de l'´ etat initial. Pendant l'exécution de l'automate sur la seconde sous-trace, un raccourci entre unétatunétat au premierélémentpremierélément de la sous-trace et l'ensemble desétatsdesétats qu'il génère au dernierélémentdernierélément de la sous-trace est calculé. Ce raccourci est ensuite utilisé pour fusionner les résultats d'analyse obtenus entre lapremì ere et la seconde sous-trace et permet de déduire le résultat global

]. Références and . Abrial, The B-book : Assigning Programs to Meanings, 1996.

F. Aguirre, M. Sallak, W. Schon, and F. Belmonte, Application of evidential networks in quantitative analysis of railway accidents, Proceedings of the Institution of Mechanical Engineers, pp.368-384, 2013.
DOI : 10.1177/1748006X12475044

URL : https://hal.archives-ouvertes.fr/hal-00749617

H. Barringer, A. Goldberg, K. Havelund, and K. Sen, Eagle does space efficient ltl monitoring, 2003.

S. Berkovich, B. Bonakdarpour, and S. Fischmeister, GPU-based Runtime Verification, 2013 IEEE 27th International Symposium on Parallel and Distributed Processing, pp.1025-1036, 2013.
DOI : 10.1109/IPDPS.2013.105

E. Bodden, Efficient hybrid typestate analysis by determining continuation-equivalent states, Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, ICSE '10, pp.5-14, 2010.
DOI : 10.1145/1806799.1806805

J. and R. Büchi, On a Decision Method in Restricted Second Order Arithmetic, The Collected Works of J. Richard Büchi, pp.425-435
DOI : 10.1007/978-1-4613-8928-6_23

E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems, vol.8, issue.2, pp.244-263, 1986.
DOI : 10.1145/5397.5399

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, 1977.
DOI : 10.1145/512950.512973

URL : https://hal.archives-ouvertes.fr/hal-01108790

M. Amorim and G. Rosu, Efficient monitoring of omega-languages, CAV'05, pp.364-378, 2005.

D. Drusinsky, The Temporal Rover and the ATG Rover, SPIN Model Checking and Software Verification, 2000.
DOI : 10.1007/10722468_19

A. Ferlin and V. Wiels, Combination of Static and Dynamic Analyses for the Certification of Avionics Software, 2012 IEEE 23rd International Symposium on Software Reliability Engineering Workshops, pp.331-336
DOI : 10.1109/ISSREW.2012.100

A. Ferlin, Vérification de propriétés temporelles sur des logiciels avioniques par analyse dynamique formelle Institut Supérieur de l'Aeronautique et de l'Espace (ISAE), 2013.

P. Gastin and D. Oddoux, Fast LTL to Büchi automata translation, Proceedings of the 13th International Conference on Computer Aided Verification (CAV'01), 2001.

M. Geimer, F. Wolf, . N. Brianj, B. Wylie, and . Mohr, Scalable Parallel Trace-Based Performance Analysis, Recent Advances in Parallel Virtual Machine and Message Passing Interface, pp.303-312, 2006.
DOI : 10.1007/11846802_43

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

D. Giannakopoulou and K. Havelund, Automata-based verification of temporal properties on running programs, Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), 2001.
DOI : 10.1109/ASE.2001.989841

K. Havelund and G. Rosu, Monitoring programs using rewriting, Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), pp.135-143, 2001.
DOI : 10.1109/ASE.2001.989799

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

K. Havelund and K. Technology, A rewriting-based approach to trace analysis, Automated Software Engineering, vol.12, 2002.

O. Patrick, D. Meredith, D. Jin, F. Griffith, G. Chen et al., An overview of the mop runtime verification framework, International Journal on Software Tools for Technology Transfer, vol.14, pp.249-289, 2012.

R. Pellizzoni, P. Meredith, M. Caccamo, and G. Rosu, Hardware Runtime Monitoring for Dependable COTS-Based Real-Time Embedded Systems, 2008 Real-Time Systems Symposium, pp.481-491, 2008.
DOI : 10.1109/RTSS.2008.43

A. Pnueli and A. Zaks, PSL Model Checking and Run-Time Verification Via Testers, FM 2006 : Formal Methods, 2006.
DOI : 10.1007/11813040_38

V. Stolz and E. Bodden, Temporal assertions using aspectj Electronic Notes in Theoretical Computer Science, Proceedings of the Fifth Workshop on Runtime Verification, pp.109-124, 2005.

H. Zhu, M. B. Dwyer, and S. Goddard, Predictable Runtime Monitoring, 2009 21st Euromicro Conference on Real-Time Systems, pp.173-183, 2009.
DOI : 10.1109/ECRTS.2009.23

C. B. Zilles and G. S. Sohi, A programmable co-processor for profiling, Proceedings HPCA Seventh International Symposium on High-Performance Computer Architecture, pp.241-252, 2001.
DOI : 10.1109/HPCA.2001.903267

P. Bieber, F. Boniol, M. Boyer, E. Noulard, and C. Pagetti, New Challenges for Future Avionic Architectures, Journal AerospaceLab, vol.4, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01184101

J. David, D. Godden, and . Walton, Advances in the theory of argumentation schemes and critical questions, Informal Logic, vol.27, issue.3, pp.267-292, 2007.

M. David, D. Godden, and . Walton, Argument from Expert Opinion as Legal Evidence: Critical Questions and Admissibility Criteria of Expert Testimony in the American Legal System, Ratio Juris, vol.19, issue.3, pp.261-286, 2006.

T. Kelly and R. Weaver, The Goal Structuring Notation ? A Safety Argument Notation, Proc. of Dependable Systems and Networks 2004 Workshop on Assurance Cases, 2004.

J. , L. Boudec, and P. Thiran, Network calculus: a theory of deterministic queuing systems for the internet, 2001.

S. Martin and P. Minet, Schedulability analysis of flows scheduled with FIFO: application to the expedited forwarding class, Proceedings 20th IEEE International Parallel & Distributed Processing Symposium, p.167, 2006.
DOI : 10.1109/IPDPS.2006.1639424

D. Ministry, Defence Standard 00-42 Issue 2, Reliability and Maintainability (R&M) Assurance Guidance Part 3 R&M Case, 2003.

T. Polacsek, Réflexions sur les liens possibles entre argumentation et v&v pour le logiciel, Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2014.

J. Sicard, G. Martinez, and F. Many, Specific Certification Issues Concerning IMA, Embedded Real-Time Software and Systems, 2012.

E. Stephen and . Toulmin, The Uses of Argument, 1958.

Y. Boichut, B. Boyer, T. Genet, and A. Legay, Equational Abstraction Refinement for Certified Tree Regular Model Checking, ICFEM'12, 2012.
DOI : 10.1007/978-3-642-34281-3_22

URL : https://hal.archives-ouvertes.fr/hal-00759149

C. H. Broadbent, A. Carayol, M. Hague, and O. Serre, C-shore : a collapsible approach to higher-order verification, ICFP'13, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00865155

G. Castagna, K. Nguyen, Z. Xu, H. Im, S. Lenglet et al., Polymorphic functions with set-theoretic types, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, 2014.
DOI : 10.1145/2535838.2535840

URL : https://hal.archives-ouvertes.fr/hal-00907166

F. Chalub and C. Braga, A Modular Rewriting Semantics for CML, J.UCS, vol.10, issue.7, pp.789-807, 2004.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973

URL : https://hal.archives-ouvertes.fr/hal-01108790

T. Genet, Towards Static Analysis of Functional Programs Using Tree Automata Completion, WRLA'14, 2014.
DOI : 10.1007/978-3-319-12904-4_8

URL : https://hal.archives-ouvertes.fr/hal-00921814

T. Genet, Y. Boichut, B. Boyer, V. Murat, and Y. Salmon, Reachability Analysis and Tree Automata Calculations. IRISA / Université de Rennes 1

T. Genet, T. L. Gall, A. Legay, and V. Murat, A Completion Algorithm for Lattice Tree Automata, CIAA'13, pp.134-145, 2013.
DOI : 10.1007/978-3-642-39274-0_13

T. Genet and R. Rusu, Equational approximations for tree automata completion, Journal of Symbolic Computation, vol.45, issue.5, pp.574-597, 2010.
DOI : 10.1016/j.jsc.2010.01.009

URL : https://hal.archives-ouvertes.fr/inria-00495405

T. Genet and Y. Salmon, Tree Automata Completion for Static Analysis of Functional Programs
URL : https://hal.archives-ouvertes.fr/hal-00780124

T. Genet and Y. Salmon, Reachability Analysis of Innermost Rewriting, RTA'15, LIPIcs. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01194530

N. D. Jones and N. Andersen, Flow analysis of lazy higher-order functional programs, Theoretical Computer Science, vol.375, issue.1-3, pp.120-136, 2007.
DOI : 10.1016/j.tcs.2006.12.030

N. Kobayashi, Model Checking Higher-Order Programs, Journal of the ACM, vol.60, issue.3, p.2013
DOI : 10.1145/2487241.2487246

L. Ong and S. Ramsay, Verifying higher-order functional programs with pattern-matching algebraic data types, POPL'11, 2011.

S. Owens, A Sound Semantics for OCamllight, ESOP'08, pp.1-15, 2008.

N. Vazou, P. Rondon, and R. Jhala, Abstract Refinement Types, ESOP'13, 2013.
DOI : 10.1007/978-3-642-37036-6_13

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

W. Wang and Z. Lu, Cyber security in the Smart Grid: Survey and challenges, Computer Networks, vol.57, issue.5, pp.1344-1371
DOI : 10.1016/j.comnet.2012.12.017

L. Zhou and S. Chen, A Survey of Research on Smart Grid Security, Network Computing and Information Security, ser. Communications in Computer and Information Science, pp.395-405
DOI : 10.1007/978-3-642-35211-9_52

A. Hamadi, M. N. Hussam, C. Yeun, and M. Zemerly, A Novel Security Scheme for the Smart Grid and SCADA Networks, Wireless Personal Communications, pp.1-13, 2013.

J. Gao, Y. Xiao, J. Liu, W. Liang, and C. L. Chen, A survey of communication/networking in Smart Grids, Future Generation Computer Systems, vol.28, issue.2, 2012.
DOI : 10.1016/j.future.2011.04.014

C. Laboratory, CEA-LIST Website

B. Bannour, J. Escobedo, C. Gaston, L. Gall, P. Pedroza et al., Designing Sequence Diagram Models for Robustness to Attacks, 2014 IEEE Seventh International Conference on Software Testing, Verification and Validation Workshops, 2014.
DOI : 10.1109/ICSTW.2014.50

M. Object and . Group, The UML standard specification

K. Koscher, A. Czeskis, F. Roesner, S. Patel, T. Kohno 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

. The-modbus-organization and . Inc, The Modbus Protocol Specification V1.1b3

L. Gall, P. Gaston, C. Escobedo, J. Bannour, . Boutheina et al., Methodology for Modeling Smart Girds Systems: Attack Impact Analysis on Interaction Scenarios The Sesam-Grids Consortium, 2013.

N. Rapin, C. Gaston, A. Lapitre, and J. Gallois, Behavioural unfolding of formal specifications based on communicating automata, Proc. of Workshop ATVA, 2003.

P. Krcal and W. Yi, Communicating Timed Automata: The More Synchronous, the More Difficult to Verify, Computer Aided Verification
DOI : 10.1007/11817963_24

B. Beizer, Black Box Testing: Techniques for Functional Testing of Software and Systems, IEEE Software, vol.13, issue.5, 1995.
DOI : 10.1109/MS.1996.536464

F. Bouquet, C. Grandpierre, B. Legeard, and F. Peureux, A test generation solution to automate software testing, Proceedings of the 3rd international workshop on Automation of software test , AST '08, pp.45-48, 2008.
DOI : 10.1145/1370042.1370052

F. Bouquet, C. Grandpierre, B. Legeard, F. Peureux, N. Vacelet et al., A subset of precise UML for model-based testing, Proceedings of the 3rd international workshop on Advances in model-based testing , A-MOST '07, pp.95-104, 2007.
DOI : 10.1145/1291535.1291545

URL : https://hal.archives-ouvertes.fr/hal-00563283

F. Dadeau, K. Cabrera-castillos, and J. Julliand, Coverage criteria for model-based testing using property patterns, 9th Workshop on Model-Based Testing, Satellite workshop of ETAPS 2014, pp.29-43, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01089687

M. B. Dwyer, G. S. Avrunin, and J. C. Corbett, Patterns in property specifications for finitestate verification, Proceedings of the 21st International Conference on Software Engineering, ICSE '99, pp.411-420, 1999.

B. Kanso and S. Taha, Temporal Constraint Support for OCL, Software Language Engineering, pp.83-103, 2013.
DOI : 10.1007/978-3-642-36089-3_6

URL : https://hal.archives-ouvertes.fr/hal-00762150

P. Cousot, R. Cousot, and J. Feret, Antoine Miné, and Xavier Rival. The astrée static analyzer, 2013.

E. Feron, From Control Systems to Control Software, IEEE Control Systems Magazine, vol.30, issue.6, pp.50-71, 2010.
DOI : 10.1109/MCS.2010.938196

V. Maisonneuve, Static Analysis of Control-Command Systems ? Floating-Point and Integer Invariants, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01155693

P. Roux, Analyse statique de système contrôle commande: synthèse d'invariants non linéaires, 2013.

A. Arusoaie, D. Lucanu, D. Nowak, and V. Rusu, Verifying Reachability-Logic Properties on Rewriting-Logic Specifications (Extended Version), Al.I.Cuza, 2015.

D. Bogd?, A. , and G. , A Complete Semantics of Java, Proceedings of the 42nd Symposium on Principles of Programming Languages (POPL'15), pp.445-456, 2015.

S. Andrei, B. M. Moore, T. Florin, S. , and G. Ro¸suro¸su, All-path reachability logic, Proceedings of the Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA'14), pp.425-440, 2014.

C. Ellison and G. Ro¸suro¸su, An executable formal semantics of C with applications, Proceedings of the 39th Symposium on Principles of Programming Languages (POPL'12), pp.533-544, 2012.

G. Ro¸suro¸su, A. S. , and B. M. Moore, One-path reachability logic, Proceedings of the 28th Symposium on Logic in Computer Science (LICS'13), pp.358-367, 2013.

G. Rosu and A. Stefanescu, Checking reachability using matching logic, Proceedings of the 27th Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOP- SLA'12), pp.555-574, 2012.

G. Rosu and A. Stefanescu, From Hoare Logic to Matching Logic Reachability, Proceedings of the 18th International Symposium on Formal Methods (FM'12), pp.387-402, 2012.
DOI : 10.1007/978-3-642-32759-9_32

. Règle-utilisateur, Detected-in(movement-in,room) Controlled-in(door,room) Has-type( ?ph,movement-in) Occurred-in( ?ph, ?loc) Perceived-type( ?s,movement-in)

B. R. Bryant, D. Johnson, and B. Edupuganty, Formal specification of natural language syntax using two-level grammar, Proceedings of the 11th coference on Computational linguistics -, pp.527-532, 1986.
DOI : 10.3115/991365.991519

A. Fougères and P. Trigano, Rédaction de spécifications formelles : élaboration à partir des spécifications écrites en langage naturel, Cognito -Cahiers Romans de Sciences Cognitives, pp.29-36, 1997.

A. Guissé, F. Lévy, and A. Nazarenko, From Regulatory Texts to BRMS: How to Guide the Acquisition of Business Rules?, RuleML 2012, pp.77-91, 2012.
DOI : 10.1007/978-3-642-32689-9_7

D. Sadoun, Des spécifications en langage naturel aux spécifications formelles via une ontologie comme modèle pivot, 2014.

D. Sadoun, C. Dubois, Y. Ghamri-doudane, and B. Grau, From Natural Language Requirements to Formal Specification Using an Ontology, 2013 IEEE 25th International Conference on Tools with Artificial Intelligence, pp.755-760, 2013.
DOI : 10.1109/ICTAI.2013.116

URL : https://hal.archives-ouvertes.fr/hal-01126372

D. Sadoun, C. Dubois, Y. Ghamri-doudane, and B. Grau, Formal Rule Representation and Verification from Natural Language Requirements Using an Ontology, RuleML 2014, pp.226-235, 2014.
DOI : 10.1007/978-3-319-09870-8_17

URL : https://hal.archives-ouvertes.fr/hal-01126517

E. Biham and A. Shamir, Differential fault analysis of secret key cryptosystems, 1997.
DOI : 10.1007/BFb0052259

D. Boneh, R. A. Demillo, and R. J. Lipton, On the Importance of Eliminating Errors in Cryptographic Computations, Journal of Cryptology, vol.14, issue.2, pp.101-119, 2001.
DOI : 10.1007/s001450010016

M. Christofi, Preuves de sécurité outillées d'implémentations cryptographiques, Thèse, 2013.

K. O. Gadellaa, Fault attacks on java card, phd thesis, technische universiteit, 2005.

X. Kauffmann-tourkestansky, Security analysis of smart card C code using simulated physical attacks. Theses, 2012.
URL : https://hal.archives-ouvertes.fr/tel-00771273

J. Quisquater and D. Samyde, ElectroMagnetic Analysis (EMA): Measures and Counter-measures for Smart Cards
DOI : 10.1007/3-540-45418-7_17

B. Marre and B. Blanc, Test Selection Strategies for Lustre Descriptions in GATeL, Electronic Notes in Theoretical Computer Science, vol.111, pp.93-111, 2005.
DOI : 10.1016/j.entcs.2004.12.010

C. Mouna-tka-mnad, I. Deleuze, and . Parissis, Synchronous programs testing language (SPTL), Computational Science and Its Applications -ICCSA 2014 -14th International Conference Proceedings, Part I, pp.683-695, 2014.

V. Papailiopoulou, B. Seljimi, and I. Parissis, Revisiting the Steam-Boiler Case Study with LUTESS : Modeling for Automatic Test Generation, Proceedings of the 12th European Workshop on Dependable Computing, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00381548

P. Raymond, D. Weber, X. Nicollin, and N. Halbwachs, Automatic testing of reactive systems, Proceedings 19th IEEE Real-Time Systems Symposium (Cat. No.98CB36279), 1998.
DOI : 10.1109/REAL.1998.739746

T. Mouna, C. Mnad, I. Deleuze, and . Parissis, Synchronous Programs Testing Language (SPTL). MSR 2013 -Modélisation des Systèmes Réactifs, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01023037

N. Huynh, M. Frappier, A. Mammar, R. Laleau, and J. Desharnais, Validating the RBAC ANSI 2012 Standard Using B, Abstract State Machines, Alloy, B, TLA, VDM, and Z -4th International Conference Proceedings, pp.255-270, 2014.
DOI : 10.1007/978-3-662-43652-3_22

URL : https://hal.archives-ouvertes.fr/hal-01264810

M. Leuschel and M. J. Butler, ProB: an automated analysis toolset for the B method, International Journal on Software Tools for Technology Transfer, vol.49, issue.3, pp.185-203, 2008.
DOI : 10.1007/s10009-007-0063-9

R. Sandhu, D. Ferraiolo, and R. Kuhn, The NIST model for role-based access control, Proceedings of the fifth ACM workshop on Role-based access control , RBAC '00, pp.47-63, 2000.
DOI : 10.1145/344287.344301

. La-fonction-ms, On peut alors appliquer le troisième théorème d'homomorphisme faible, et on obtient que ms est l'homomorphisme , f avec f a = (mps ? (a + mps s ) (b m , b s ) = ms(ms (a m , a s ) ++ ms (b m , b s )) =

. En-définissant-la-classe-rightinverse-par, AFADL 2015 ? Résumés d'articles déjà publiés Class Right_inverse '(h:list A ?B)(h':B?list A) := { right_inverse: ?l, h l = h(h'(h l)) }

J. Gibbons, Abstract, Journal of Functional Programming, vol.43, issue.04, pp.657-665, 1996.
DOI : 10.1016/S0004-3702(78)80016-2

Z. Hu, M. Takeichi, and W. Chin, Parallelization in calculational forms, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.316-328, 1998.
DOI : 10.1145/268946.268972

F. Loulergue, F. Gava, and D. Billiet, Bulk Synchronous Parallel ML: Modular Implementation and Performance Prediction, International Conference on Computational Science (ICCS) References [1] Andrei Arusoaie, Dorel Lucanu, David Nowak, and Vlad Rusu. Verifying Reachability-Logic Properties on Rewriting-Logic Specifications, submitted to Festschrift Symposium in Honor of Jose Meseguer: Logic, Rewriting, and Concurrency, pp.1046-1054, 2005.
DOI : 10.1007/11428848_132