J. Barnat, L. Brim, and P. Simecek, Cluster-based I/O-efficient LTL model checking, Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, pp.635-639, 2009.

J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, and W. Yi, UPPAAL -a tool suite for automatic verification of real-time systems, HS 1995, vol.1066, pp.232-243, 1996.

B. Berthomieu, Fiacre: an intermediate language for model verification in the topcased environment, European Congress on Embedded Real-Time Software (ERTS). SEE, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00262442

B. Berthomieu, S. Dal-zilio, and L. Fronc, Model-checking real-time properties of an aircraft landing gear system using fiacre, ABZ 2014. CCIS, vol.433, pp.110-125, 2014.
URL : https://hal.archives-ouvertes.fr/hal-00967422

F. Boniol, P. Dhaussy, L. Le-roux, and J. C. Roger, Model-based analysis, Embedded systems, Analysis and Modeling with SysML, UML and AADL, pp.157-184, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00843139

F. Boniol, V. Wiels, F. Boniol, V. Wiels, and Y. Ait-ameur, The landing gear system case study, ABZ 2014. CCIS, vol.433, pp.1-18, 2014.

J. Burch, E. Clarke, K. Mcmillan, D. Dill, and L. Hwang, Symbolic model checking: 10 20 states and beyond, Inf. Comput, vol.98, issue.2, p.90017, 1992.

E. M. Clarke, E. A. Emerson, and A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Trans. Program. Lang. Syst, vol.8, issue.2, pp.244-263, 1986.

E. M. Clarke, R. Enders, T. Filkorn, and S. Jha, Exploiting symmetry in temporal logic model checking, Formal Methods Syst. Des, vol.9, issue.1, pp.77-104, 1996.

E. Clarke, A. Biere, R. Raimi, and Y. Zhu, Bounded model checking using satisfiability solving, Formal Methods Syst. Des, vol.19, issue.1, pp.7-34, 2001.

E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Logic of Programs 1981, vol.131, pp.52-71, 1982.

P. Dhaussy, F. Boniol, and E. Landel, Using context descriptions and property definition patterns for software formal verification, Proceedings of the 2008 IEEE International Conference on Software Testing Verification and Validation Workshop, pp.89-96, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00517276

P. Dhaussy, F. Boniol, J. C. Roger, and L. Le-roux, Improving model checking with context modelling, Advances in Software Engineering, vol.13, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00738735

P. Dhaussy, P. Pillain, S. Creff, A. Raji, Y. Le-traon et al., Evaluating context descriptions and property definition patterns for software formal validation, MODELS 2009, vol.5795, pp.438-452
URL : https://hal.archives-ouvertes.fr/hal-00635653

, , 2009.

P. Dhaussy, C. Teodorov, F. Boniol, V. Wiels, and Y. Ait-ameur, Context-aware verification of a landing gear system, ABZ 2014. CCIS, vol.433, pp.52-65, 2014.

X. Dumas, P. Dhaussy, F. Boniol, and E. Bonnafous, Application of partial-order methods for the verification of closed-loop SDL systems, Proceedings of the 2011 ACM Symposium on Applied Computing, pp.1666-1673, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00635533

P. Godefroid, The Ulg partial-order package for SPIN, SPIN Workshop, 1995.

G. J. Holzmann, The model checker SPIN, IEEE Trans. Softw. Eng, vol.23, issue.5, pp.279-295, 1997.

D. Kroening, O. Strichman, L. D. Zuck, P. C. Attie, and A. Cortesi, Efficient computation of recurrence diameters, VMCAI 2003, vol.2575, pp.298-309, 2003.

P. Parizek and F. Plasil, Specification and generation of environment for model checking of software components, Electron. Notes Theor. Comput. Sci, vol.176, issue.2, pp.143-154, 2007.

S. Park and G. Kwon, Avoidance of state explosion using dependency analysis in model checking control flow model, ICCSA 2006, vol.3984, p.99, 2006.

D. Peled, Combining partial order reductions with on-the-fly model-checking. Formal Methods Syst, Des, vol.8, issue.1, pp.39-64, 1996.

J. P. Queille and J. Sifakis, Specification and verification of concurrent systems in CESAR, 1982.

, LNCS, vol.137, pp.337-351, 1982.

C. Teodorov, P. Dhaussy, and L. Le-roux, Environment-driven reachability for timed systems, Int. J. Softw. Tools Technol. Transfer, vol.19, issue.2, pp.229-245, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01373335

C. Teodorov, L. Le-roux, and P. Dhaussy, Context-aware verification of a cruisecontrol system, MEDI 2014, vol.8748, pp.53-64, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01203701

C. Teodorov, L. Le-roux, Z. Drey, and P. Dhaussy, Past-free[ze] reachability analysis: reaching further with DAG-directed exhaustive state-space analysis, Softw. Test. Verif. Reliab, vol.26, issue.7, pp.516-542, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01373287

O. Tkachuk and M. B. Dwyer, Environment generation for validating event-driven software using model checking, IET Softw, vol.4, issue.3, pp.194-209, 2010.

A. Valmari, Stubborn sets for reduced state space generation, ICATPN 1989, vol.483, pp.491-515, 1991.

V. Wiels, E. Ledinot, E. Belin, and M. Dassault, Experiences in using model checking to verify real time properties of a landing gear control system, Embedded Real-Time Systems (ERTS), 2006.
URL : https://hal.archives-ouvertes.fr/hal-02270431

K. Yatake and T. Aoki, Automatic generation of model checking scripts based on environment modeling, Model Checking Software -17th International SPIN Workshop, pp.58-75, 2010.

Y. Yu, P. Manolios, and L. Lamport, Model checking TLA + specifications, CHARME 1999, vol.1703, pp.54-66, 1999.