H. , D. Evtackhmi, and A. Externalmassstorage, Les éléments constituants les phrases font partie du vocabulaire du domaine

. Une-exigence-est-définie-dans-un-contexte-particulier, Autrement dit, elle doit être vérifiée sous des conditions particulières. 7.2, GÉNÉRATION DES PROPRIÉTÉS CDL À PARTIR DES EXIGENCES URM

G. Des and P. Urm, Une partie dite manuelle, où l'expert du domaine est en charge de produire les modèles de sortie de l'activité. Cette partie, englobe les activités de spécification et de consolidation des exigences de la figure 7.4 ainsi que l'activité de rectification

. Ensuite, Le mot clé then est suivie d'une phrase simple affirmative indiquant que l'exigence correspond à un "patron réponse

. Ainsi, 1, la structure de l'exigence AFS-SM-020 est la suivante, pp.1-2

&. Bibliography-[-almendros-jimenez, ]. Iribarn, and L. Iribarn, Describing use cases with activity charts, Metainformatics, vol.3511, pp.153-167, 2005.

. Alur, Partial-order reduction in symbolic state space exploration, Computer Aided Verification, pp.340-351, 1997.
DOI : 10.1007/3-540-63166-6_34

. Alur, Inference of message sequence charts, Proceedings of the International Conference on Software Engineering, pp.304-313, 2000.

&. Ambriola, V. Ambriola, and . Gervasi, On the Systematic Analysis of Natural Language Requirements with CIRCE, Automated Software Engineering, vol.20, issue.6, pp.107-167, 2006.
DOI : 10.1007/s10515-006-5468-2

. Berthomieu, The tool TINA ??? Construction of abstract state spaces for petri nets and time petri nets, International Journal of Production Research, vol.99, issue.14, pp.298-304, 2004.
DOI : 10.1137/0216062

. Berthomieu, The syntax and semantics of Fiacre, p.35, 2007.

. Berthomieu, Fiacre: an Intermediate Language for Model Verification in the Topcased Environment, p.121, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00262442

A. Bertolino, Formal Methods for Software Architectures, volume VII of 978-3-540-20083-3, Third International School on Formal Methods for the Design of Computer, Communication and Software Systems: Software Architectures , SFM 2003, p.137, 2003.

. Booch, The Unified Modeling Language User Guide, pp.30-115, 1999.

&. Bosnacki, . Holzmann-dragan, G. J. Bosnacki, and . Holzmann, Improving Spin's Partial-Order Reduction for Breadth-First Search, SPIN, pp.91-105, 2005.

. Bozga, IF: An Intermediate Representation for SDL and its Applications, SDL Forum, pp.423-440, 1999.
DOI : 10.1016/B978-044450228-5/50028-X

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

&. Broy and . Slotosch, Manfred Broy et Oscar Slotosch Enriching the Development Process with Formal Methods, pp.44-61, 1999.

&. Broy and . Slotosch, Manfred Broy et Oscar Slotosch. From Requirements to Validated Embedded Systems, pp.51-65, 2001.

]. R. Buhr, Use case maps as architectural entities for complex systems, IEEE Transactions on Software Engineering, vol.24, issue.12, pp.1131-1155, 1998.
DOI : 10.1109/32.738343

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

]. J. Carroll, Scenario-based design: envisioning work and technology in system development, p.70, 1995.

. Cheng, Research Directions in Requirements Engineering, Future of Software Engineering (FOSE '07), pp.285-303, 2007.
DOI : 10.1109/FOSE.2007.17

. Cimatti, NUSMV: a new symbolic model checker, International Journal on Software Tools for Technology Transfer (STTT), vol.2, issue.4, pp.410-425, 2000.
DOI : 10.1007/s100090050046

. Clarke, 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

. Colombo, A Methodological Framework for SysML: a Problem Frames-based Approach, 14th Asia-Pacific Software Engineering Conference (APSEC'07), p.115, 2007.
DOI : 10.1109/ASPEC.2007.56

. Craigen, Formal methods reality check: industrial usage, IEEE Transactions on Software Engineering, vol.21, issue.2, pp.90-98, 1995.
DOI : 10.1109/32.345825

A. Russo, O. Dalal, A. , and S. Uchitel, Extracting Requirements from Scenarios with ILP, Inductive Logic Programming, pp.1-15, 2007.

&. Darimont, . Van-lamsweerde, . Darimont, and . Van-lamsweerde, Formal refinement patterns for goal-driven requirements elaboration, ACM SIGSOFT Software Engineering Notes, vol.21, issue.6, pp.190-82, 1996.
DOI : 10.1145/239098.239131

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

]. A. Davis, Software requirements: objects, functions and states, 1993.

D. Denger, . Berry, and . Kamsties, Higher quality requirements specifications through natural language patterns. Software: Science, Technology and Engineering, SwSTE'03. Proceedings. IEEE International Conference on, pp.80-90, 2003.
DOI : 10.1109/swste.2003.1245428

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

&. Dhaussy and . Boniol, Philippe Dhaussy et Frédéric Boniol Mise en oeuvre de composants MDA pour la validation formelle de modèles de systèmes d'information embarqués, Revue des Sciences et Techniques Informatiques, pp.133-157, 2007.

&. Dhaussy, J. Dhaussy, and . Roger, CDL (Context Description Language) : Syntax and semantics, p.37, 2011.

. Dhaussy, Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation, ACM/IEEE 12th International Conference on Model Driven Engineering Languages and Systems, pp.438-452, 2009.
DOI : 10.1007/978-1-4612-0931-7

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

. Dhaussy, Reducing State Explosion with Context Modeling for Model-Checking, 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering, p.44, 2011.
DOI : 10.1109/HASE.2011.24

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

. Dwyer, Patterns in property specifications for finite-state verification, 21st Int. Conf. on Software Engineering, pp.411-420, 1999.

A. Emerson, S. Jha, D. A. Peled-]-e, S. Emerson, D. Jha et al., Combining Partial Order and Symmetry Reductions Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol.1217, issue.4, pp.19-34, 1997.

H. Ebner and . Kaindl, Tracing all around in reengineering, IEEE Software, vol.19, issue.3, pp.70-77, 2002.
DOI : 10.1109/MS.2002.1003459

M. Flanzer, J. Terry, and . Landa, RECAP: a requirements elicitation, capture and analysis process prototype tool for large complex systems, IEEE International Conference on Engineering of Complex Computer Systems, pp.6-10, 1995.

. Fabbrini, The linguistic approach to the natural language requirements quality: benefit of the use of an automatic tool, Proceedings 26th Annual NASA Goddard Software Engineering Workshop, pp.97-105, 2001.
DOI : 10.1109/SEW.2001.992662

. Fantechi, Assisting requirement formalization by means of natural language translation, Formal Methods in System Design, p.82, 1994.
DOI : 10.1007/BF01384048

. Farail, The TOPCASED project : a Toolkit in OPen source for Critical Aeronautic SystEms Design, 3rd European Congress EMBEDDED REAL TIME SOFTWARE (ERTS), p.40, 2006.

. Farail, FIACRE: an intermediate language for model verification in the TOPCASED environment, European Congress on Embedded Real-Time Software (ERTS), pp.2008-2009, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00262442

&. Feiler, . H. Humphrey-1993-]-p, W. S. Feiler, and . Humphrey, Software process development and enactment: concepts and definitions, [1993] Proceedings of the Second International Conference on the Software Process-Continuous Software Process Improvement, pp.28-40, 1993.
DOI : 10.1109/SPCON.1993.236824

URL : http://www.dtic.mil/get-tr-doc/pdf?AD=ADA258465

. Fernandez, CADP a protocol validation and verification toolbox, CAV '96: Proceedings of the 8th International Conference on Computer Aided Verification, pp.437-440, 1996.
DOI : 10.1007/3-540-61474-5_97

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

&. Ferreira, A. Rodrigues-da-silva-david-de-almeida-ferreira, . Rodrigues, and . Silva, A Controlled Natural Language Approach for Integrating Requirements and Model-Driven Engineering, 2009 Fourth International Conference on Software Engineering Advances, pp.518-523, 2009.
DOI : 10.1109/ICSEA.2009.81

&. Finkelstein, J. Kramer-anthony-finkelstein, and . Kramer, Software engineering, Proceedings of the conference on The future of Software engineering , ICSE '00, p.24, 2000.
DOI : 10.1145/336512.336519

. Fuchs, Attempto Controlled English? not just another logic specification language. Logic-Based Program Synthesis and Transformation, pp.1-20, 1999.
DOI : 10.1007/3-540-48958-4_1

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

. Genest, Message Sequence Charts, Application of Concurrency to System Design, 2005. ACSD 2005. Fifth International Conference on, pp.2-4, 2005.
DOI : 10.1007/978-3-540-27755-2_15

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

. Godefroid, Patrice Godefroid, Doron Peled et Mark G. Staskauskas. Using Partial-Order Methods in the Formal Validation of Industrial Concurrent Programs, International Symposium on Software Testing and Analysis, pp.261-269, 1996.

. Gutiérrez, Visualization of Use Cases through Automatically Generated Activity Diagrams, MoDELS, vol.5301, pp.83-96, 2008.
DOI : 10.1007/978-3-540-87875-9_6

&. Kugler-1999, ]. D. Harel, and H. Kugler, Synthesizing State-Based Object Systems from LSC Specifications, p.70, 1999.

. Hassine, An evaluation of timed scenario notations, Journal of Systems and Software, vol.83, issue.2, pp.326-350, 2010.
DOI : 10.1016/j.jss.2009.09.014

. Haugen, Oystein Haugen, Knut Eilif Husa, Ragnhild Kobro Runde et Ketil Stolen. STAIRS towards formal design with sequence diagrams, Software and System Modeling, pp.355-357, 2005.

. Heitmeyer, On the need for practical formal methods. Formal Techniques in Real-Time and Fault-Tolerant Systems, Proc., 5th Intern. Symposium, pp.18-26, 1998.

. Heymer, A semantics for MSC based on petri net components, 4th International SDL and MSC Workshop (SAM'00), pp.1-15, 2000.

]. G. Holzmann, The model checker SPIN, IEEE Transactions on Software Engineering, vol.23, issue.5, pp.279-295, 1997.
DOI : 10.1109/32.588521

. Holzmann, The SPIN Model Checker, Primer and Reference Manual, p.29, 2004.

E. Kaindli and . Software, Difficulties in the transition from OO analysis to design, IEEE Software, vol.16, issue.5, pp.94-102, 1999.
DOI : 10.1109/52.795107

L. Kof, Natural Language Processing to Requirements Engineering: Applicability to large requirements documents. Citeseer, p.53, 2004.

&. Konrad, ]. S. Cheng-2005a, B. Konrad, and . Cheng, Real-Time Specification Patterns.I n 27th Int, Conf. on Software Engineering (ICSE05), pp.39-107, 2005.

&. Konrad, S. Cheng, . Konrad, H. Betty, and . Cheng, Real-time Specification Patterns, International Conference on Software Engineering, pp.372-381, 2005.
DOI : 10.1109/icse.2005.1553580

&. Konrad, H. Betty, and . Cheng, Facilitating the construction of specification pattern-based properties, 13th IEEE International Conference on Requirements Engineering (RE'05), p.24, 2005.
DOI : 10.1109/RE.2005.29

&. Konrad, H. Betty, and . Cheng, Automated Analysis of Natural Language Properties for UML Models, International Conference on Model Driven Engineering Languages and Systems, pp.48-57, 2006.
DOI : 10.1007/11663430_6

&. Koskimies, . Mlkinen, E. Koskimies, and . Mlkinen, Automatic synthesis of state machines from trace diagrams. Software Practice and Experience, pp.643-658, 1994.

&. Peter, B. Ladkin, and S. Leue, Interpreting Message Flow Graphs, Formal Aspects of Computing, vol.7, issue.70, pp.473-509, 1995.

]. A. Van-lamsweerde, Requirements engineering, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, SIGSOFT '08/FSE-16, p.712, 2009.
DOI : 10.1145/1453101.1453133

. Larsen, Uppaal in a nutshell, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, pp.134-152, 1997.
DOI : 10.1007/s100090050010

. Lee, Handbook of real-time and embedded systems, Chapman & Hall/CRC, issue.3, 2007.

. Lu, A Requirement Tool to Support Model-Based Requirement Engineering, 2008 32nd Annual IEEE International Computer Software and Applications Conference, pp.712-717, 2008.
DOI : 10.1109/COMPSAC.2008.232

&. Millan, ]. K. Probst, . Mc, D. K. Millan, and . Probst, A Technique of State Space Search Based on Unfolding, Formal Methods in System Design, pp.45-65, 1992.

A. George and . Miller, WordNet: A Lexical Database for English, Communications of the ACM, pp.39-41, 1995.

]. G. Mullery, Core-A method for controlled requirements specification.I n The Institution of Eletrical Engineers, 4th International Conference on Software Engineering, pp.126-125, 1979.

. Mustafiz, Addressing degraded service outcomes and exceptional modes of operation in behavioural models, Proceedings of the 2008 RISE/EFTS Joint International Workshop on Software Engineering for Resilient Systems, SERENE '08, p.67, 2008.
DOI : 10.1145/1479772.1479776

P. Allen, G. Nikora, and . Balcom, Automated Identification of LTL Patterns in Natural Language Requirements, Software Reliability Engineering, International Symposium on, pp.185-194, 2009.

K. Övergaard and . Palmkvist, A formal approach to use cases and their relationships. The Unified Modeling Language UML'98: Beyond the Notation, pp.514-514, 2004.

&. Park, ]. S. Kwon, G. Park, and . Kwon, Avoidance of State Explosion Using Dependency Analysis in Model Checking Control Flow Model, LNCS, issue.4, 2006.
DOI : 10.1007/11751649_99

&. Queille, J. Queille, and . Sifakis, Specification and verification of concurrent systems in CESAR, Proceedings of the 5th Colloquium on International Symposium on Programming, pp.337-351, 1982.
DOI : 10.1007/3-540-11494-7_22

&. Raji, P. Dhaussy-2010a-]-amine-raji, and . Dhaussy, Automatic Formal Model Derivation from Use Cases In 6èmes journées sur l'Ingénierie Dirigée par les ModèlesAdour (UPPA). xvii [Raji & Dhaussy 2010b] Amine Raji et Philippe Dhaussy User Context Models: A Framework to Ease Software Formal Verifications Modèles orientés utilisateurs pour la vérification formelle en contexte industriel Improving formal verification practicability through user oriented models and context-awareness, 12th International Conference on Enterprise Information Systems 7ème journées sur l'Ingénierie Dirigée par les Modèles (IDM) 2011. xvii [Raji & Dhaussy 2011b] Amine Raji et Philippe Dhaussy Proceedings of the 8th International Workshop on Model-Driven Engineering, Verification and Validation, pp.1-8, 2010.

&. Raji, P. Dhaussy-2011c-]-amine-raji, and V. Dhaussy, Use Cases Modeling for Scalable Model-Checking Automating Context Description for Software Formal Verification, The 18th Asian Pacific Software Engineering Conference (APSEC) MODEVVA '10: Proceedings of the Workshop on Model-Driven Engineering, Verification, and Validation, pp.65-72, 1999.

]. Roger, Exploitation de contextes et d'observateurs pour la validation formelle de modËles, p.45, 2006.

. Rosenblum, Formal methods and testing, ACM SIGSOFT Software Engineering Notes, vol.21, issue.4, p.24, 1996.
DOI : 10.1145/232069.232086

. Shui, Exceptional Use Cases, 8th International Conference on Model Driven Engineering Languages and Systems, pp.568-583, 2005.
DOI : 10.1007/11557432_43

URL : https://hal.archives-ouvertes.fr/lirmm-00106504

. Shui, Exception-aware requirements elicitation with use cases Advanced Topics in Exception Handling, LNCS, vol.4119, pp.221-242, 2006.

. Smith, PROPEL, Proceedings of the 24th international conference on Software engineering , ICSE '02, pp.11-21, 2002.
DOI : 10.1145/581339.581345

&. Sommerville, P. Sawyer-ian-sommerville, and . Sawyer, Viewpoints: principles, problems and a practical approach to requirements engineering, Annals of Software Engineering, vol.3, pp.101-130, 1997.
DOI : 10.1023/A:1018946223345

P. Putnan, . Texel, B. Charles, and . Williams, Use cases combined with BOOCH/OMT/UML: Process and products, volume 978-0137274055, 465 pages, p.23, 1997.

S. Uchitel, J. Kramer, and J. Magee, Incremental elaboration of scenario-based specifications and behavior models using implied scenarios, ACM Transactions on Software Engineering and Methodology, vol.13, issue.1, pp.37-85, 2004.
DOI : 10.1145/1005561.1005563

&. Lamsweerde, E. Van-lamsweerde, and . Letier, From Object Orientation to Goal Orientation: A Paradigm Shift for Requirements Engineering, Radical Innovations of Software & System Engineering LNCS, pp.4-8, 2004.
DOI : 10.1007/978-3-540-24626-8_23

. Lamsweerde and . Van-lamsweerde, Requirements engineering, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, SIGSOFT '08/FSE-16, pp.238-249, 2008.
DOI : 10.1145/1453101.1453133

&. Videira, C. Rodrigues-da-silva, A. Videira, . Rodrigues, and . Silva, Patterns and metamodel for a natural-language-based requirements specification language, CaiSE Forum, pp.25-27, 2005.

. Videira, The ProjectIT-RSL Language Overview, Satellite Activities, vol.3297, pp.269-272, 2005.
DOI : 10.1007/978-3-540-31797-5_31

]. Whittle and . Jayaraman, Generating Hierarchical State Machines from Use Case Charts, 14th IEEE International Requirements Engineering Conference (RE'06), pp.19-28, 2006.
DOI : 10.1109/RE.2006.25

. Williams, Toward Engineered, Useful Use Cases., The Journal of Object Technology, vol.4, issue.6, pp.45-57, 2005.
DOI : 10.5381/jot.2005.4.6.a4

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

. Wolter, Reusing Terminology for Requirements Specifications from WordNet.I n, 16th IEEE International Requirements Engineering Conference (RE), pp.325-326, 2008.
DOI : 10.1109/re.2008.56

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

T. Yue, L. Briand, and Y. Labiche, A systematic review of transformation approaches between user requirements and analysis models, Requirements Engineering, vol.32, issue.2, pp.75-99, 2010.
DOI : 10.1007/s00766-010-0111-y

H. Zhu and . Jin, Automating scenario-driven structured requirements engineering, Computer Software and Applications Conference The 24th Annual International, pp.311-316, 2000.

. Zhu, Software requirements validation via task analysis, Journal of Systems and Software, vol.61, issue.2, pp.145-169, 2002.
DOI : 10.1016/S0164-1212(01)00109-1

. Ziadi, Tewfik Ziadi, Xavier Blanc et Amine RAJI. From Requirements to Code Revisited, ISORC '09: Proceedings of the 2009 IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing, pp.228-235, 2009.