@inproceedings{albore2017IMBSA,
	title={A Model-Checking Approach to Analyse Temporal Failure Propagation with {A}lta{R}ica},
	author={Albore, Alexandre and Dal Zilio, Silvano and Infantes, Guillaume and Seguin, Christel and Virelizier, Pierre},
	booktitle={International Symposium on Model-Based Safety and Assessment -- LNCS},
	pages={147--162},
	year={2017},
	volume={10437},
	organization={Springer}
}

@inproceedings{albore2018ERTS,
	title={Timed Formal Model and Verification of Satellite {FDIR} in Early Design Phase},
	author={Albore, Alexandre and Dal Zilio, Silvano and de Roquemaurel, Marie and Seguin, Christel and Virelizier, Pierre},
	booktitle={9th European Congress on Embedded Real Time Software and Systems},
	OPTpages={147--162},
	year={2018},
	address={Toulouse, France}
}


@article{nusmv,
	title={{NuSMV}: a new symbolic model checker},
	author={Cimatti, Alessandro and Clarke, Edmund and Giunchiglia, Fausto and Roveri, Marco},
	journal={International Journal on Software Tools for Technology Transfer},
	volume={2},
	number={4},
	pages={410--425},
	year={2000},
	publisher={Springer}
}

@article{bozzano2010safety,
	title={Safety, dependability and performance analysis of extended AADL models},
	author={Bozzano, Marco and Cimatti, Alessandro and Katoen, Joost-Pieter and Nguyen, Viet Yen and Noll, Thomas and Roveri, Marco},
	journal={The Computer Journal},
	volume={54},
	number={5},
	pages={754--775},
	year={2010},
	publisher={Oxford University Press}
}

@inproceedings{PRISM,
	title={PRISM 4.0: Verification of Probabilistic Real-time Systems},
	author={Kwiatkowska, Marta and Gethin, Norman and Parker, David},
	booktitle={International Conference on Computer Aided Verification (CAV’11) -- LNCS},
	pages={585-591},
	year={2011},
	volume={6806},
	organization={Springer}
}

@inproceedings{brunel2017performing,
	title={Performing Safety Analyses with AADL and AltaRica},
	author={Brunel, Julien and Feiler, Peter and Hugues, J{\'e}r{\^o}me and Lewis, Bruce and Prosvirnova, Tatiana and Seguin, Christel and Wrage, Lutz},
	booktitle={International Symposium on Model-Based Safety and Assessment -- LNCS},
	pages={67--81},
	year={2017},
		volume={10437},
	organization={Springer}
}

@article{KNP04b,
	author={M. Kwiatkowska and G. Norman and D. Parker},
	title={Probabilistic Symbolic Model Checking with {PRISM}: A Hybrid Approach},
	journal={International Journal on Software Tools for Technology Transfer (STTT)},
	year={2004},
	volume={6},
	number={2},
	pages={128--142}
}

@Article{arn00,
  author = 	 {Arnold, A. and Griffault, A. and Point, G. and Rauzy, A.},
  title = 	 {The {AltaRica} formalism for describing concurrent systems },
  journal = 	 {Fundamenta Informatic{\ae}},
  year = 	 {2000},
  volume = 	 {40},
  number={2, 3},
  publisher={IOS Press},
  pages = 	 {109-124}
}

@book{Stamatis,
	author = {Stamatis, D. H.},
	title = {Failure {M}ode and {E}ffect Analysis: {FMEA} from Theory to Execution},
	date = {2003},
	publisher = {ASQ Quality Press}
}

@article{papadopoulos2011engineering,
	title={Engineering failure analysis and design optimisation with {H}i{P}-{HOPS}},
	author={Papadopoulos, Yiannis and Walker, Martin and Parker, David and R{\"u}de, Erich and Hamann, Rainer and Uhlig, Andreas and Gr{\"a}tz, Uwe and Lien, Rune},
	journal={Engineering Failure Analysis},
	volume={18},
	number={2},
	pages={590--608},
	year={2011},
	publisher={Elsevier}
}

@phdthesis{walker2009pandora,
	title={Pandora: a logic for the qualitative analysis of temporal fault trees},
	author={Walker, Martin David},
	year={2009},
	school={The University of Hull}
}
@article{pagetti2004,
  title={A timed extension for {A}lta{R}ica},
  author={Cassez, Franck and Pagetti, Claire and Roux, Olivier},
  journal={Fundamenta Informatic{\ae}},
  volume={62},
  number={3-4},
  pages={291--332},
  year={2004},
  publisher={IOS Press}
}

@article{stamatelatos2002fault,
	title={Fault tree handbook with aerospace applications},
	author={Stamatelatos, Michael and Vesely, William and Dugan, Joanne and Fragola, Joseph and Minarick, Joseph and Railsback, Jan},
	year={2002},
	publisher={{NASA}, Washington, DC}
}

@book{FMEA,
	author = {United States military procedure MIL-P-1629},
	title = {Procedure for performing a failure mode effect and criticality analysis},
	date = {1949}
}


@inproceedings{figaro,
	author = {Bouissou, M},
	title = {Automated dependability analysis of complex systems with the KB3 workbench: the experience of EDF R\&D},
	booktitle = {Proceedings of CIEM},
	date = {2005},
	OPTeventtitle = {eventtitle},
	eventdate = {22–25 October 2005},
	venue = {Bucharest, Romania}
}

@inproceedings{daws,
	author = { Daws, C. and Yovine, S.},
	editor = {IEEE},
	title = {Reducing the Number of Clock Variables of Timed Automata},
	booktitle = {17th IEEE Real-Time Systems Symposium},
	date = {1996},
	venue = {Washington, DC}

}

@article{uppaal1997,
	author = {K. G. Larsen and P. Pettersson and W. Yi},
	title = {UPPAAL in a nutshell},
	journaltitle = {International Journal on Software Tools for Technology Transfer (STTT)},
	date = {1997},
	volume = {1},
	number = {1},
	pages = {134-152}
}

@inproceedings{uppaal2006,
  title={{UPPAAL} 4.0},
  author={Behrmann, Gerd and David, Alexandre and Larsen, Kim Guldstrand and Hakansson, John and Petterson, Paul and Yi, Wang and Hendriks, Martijn},
  booktitle={Quantitative Evaluation of Systems, 2006 (QEST 2006)},
  pages={125--126},
  year={2006},
  organization={IEEE}
}

@article{bernard2007experiments,
  title={Experiments in model based safety analysis: {F}light controls},
  author={Bernard, Romain and Aubert, Jean-Jacques and Bieber, Pierre and Merlini, Christophe and Metge, Sylvain},
  journal={IFAC Proceedings Volumes},
  volume={40},
  number={6},
  pages={43--48},
  year={2007},
  publisher={Elsevier}
}
@inproceedings{bieber2002combination,
  title={Combination of fault tree analysis and model checking for safety assessment of complex system},
  author={Bieber, Pierre and Castel, Charles and Seguin, Christel},
  booktitle={European Dependable Computing Conference},
  pages={19--31},
  year={2002},
  organization={Springer}
}
@InProceedings{poi99,
  author = 	 {Point, G. and Rauzy, A.},
  title = 	 {{AltaRica} - Langage de mod{\'e}lisation par automates \`a contraintes},
  booktitle = {Actes du Congr\'es Mod\'elisation des Syst\`emes R\'eactifs},
  year = 	 {1999},
  publisher = 	 {Herm\`es ed.}
}

@InProceedings{rauzy02,
  author = 	 {Rauzy, A.},
  title = 	 {Mode automata and their compilation into fault trees},
  booktitle = {Reliability Engineering and 
System Safety},
  year = 	 {2002}
}

@incollection{bieber2004safety,
  title={Safety assessment with {A}ltarica},
  author={Bieber, Pierre and Bougnol, Christian and Castel, Charles and Kehren, Jean-Pierre Heckmann Christophe and Metge, Sylvain and Seguin, Christel},
  booktitle={Building the Information Society},
  pages={505--510},
  year={2004},
  publisher={Springer}
}

@Article{rau08,
  author = 	 {Rauzy A.},
  title = 	 {Guarded {T}ransition {S}ystems: a new States/Events Formalism for Reliability Studies},
  journal =  {Journal of Risk and Reliability},
  year = 	 {2008},
  volume = 	 {222},
  number = 	 {4}
}

@article{prosvirnova2013altarica,
  title={The {A}lta{R}ica 3.0 project for {M}odel-{B}ased {S}afety {A}ssessment},
  author={Prosvirnova, Tatiana and Batteux, Michel and Brameret, Pierre-Antoine and Cherfi, Abraham and Friedlhuber, Thomas and Roussel, Jean-Marc and Rauzy, Antoine},
  journal={IFAC Proceedings Volumes},
  volume={46},
  number={22},
  pages={127--132},
  year={2013},
  publisher={Elsevier}
}

@inproceedings{thomas2013,
  title={Model-Based {RAMS} \& {FDIR} Co-Engineering at {A}strium Satellites},
  author={Thomas, Dave and Blanquart, Jean-Paul},
  booktitle={Data System In Aerospace (DASIA 2013)},
  publisher ={ESA Special Publication},
  volume={720},
  pages={33},
  year={2013}
}

@article{arnold1999altarica,
  title={The {AltaRica} formalism for describing concurrent systems},
  author={Arnold, Andr{\'e} and Point, G{\'e}rald and Griffault, Alain and Rauzy, Antoine},
  journal={Fundamenta Informaticae},
  volume={40},
  number={2, 3},
  pages={109--124},
  year={1999},
  publisher={IOS Press}
}

@inproceedings{bouissou05,
	author = { Bouissou, M.},
	title = {Automated dependability analysis of complex systems with the KB3 workbench: the experience of EDF R\&D},
	booktitle = {International Conference on ENERGY and ENVIRONMENT (CIEM)},
	year = {2005}
}

@inproceedings{bittner2014,
	author = {Bittner, B. and  Bozzano, M. and Cimatti,  A. and De Ferluc, R. and Gario, M. and Guiotto, A. and Yushtein, Y.},
	title = {An Integrated Process for {FDIR} Design in Aerospace},
	booktitle = {International Symposium on Model Based Safety and Assessment (IMBSA)},
	year = {2014},
	venue = {Trento}
}

@booklet{arc,
	author = {Point, G. and Griffault, A. and  Vincent, A.},
	title = {AltaRica Checker Handbook - A user-guide to ARC version 1},
	year = {2010},
	location = {Talence: LaBRI - CNRS UMR 5800 - Univ. de Bordeaux}
}

@report{Griffault06,
	author = {Griffault, A. and Point, G.},
	title = {On the partial translation of {L}ustre programs into the {A}lta{R}ica language and vice versa},
	type = {Research Report},
	institution = {LaBRI - CNRS UMR 5800},
	year = {2006},
    number = {1415-06},
	location = {Bordeaux}
}


@inproceedings{mec5,
	author = {A. Griffault and A. Vincent},
	title = {The {MEC} 5 model-checker},
	booktitle = {International Conference on Computer Aided Verification},
	year = {2004}
}

@inproceedings{rugina09,
	author = {A.-E. Rugina and J.-P. Blanquart and R. Soumagne},
	title = {Validating {F}ailure {D}etection {I}solation and {R}ecovery {S}trategies using {T}imed {A}utomata},
	booktitle = {12th European Workshop on Dependable Computing (EWDC 2009)},
	year = {2009},
	venue = {Toulouse}
}

@inproceedings{chaki2004,
	title={State/event-based Software Model Checking},
	author={Chaki, Sagar and Clarke, Edmund M. and Ouaknine, Jo{\"e}l and Sharygina, Natasha and Sinha, Nishant},
	booktitle={International Conference on Integrated Formal Methods},
	pages={128--147},
	year={2004},
	organization={Springer}
}

@inproceedings{cadp,
	title={CADP a protocol validation and verification toolbox},
	author={Fernandez, Jean-Claude and Garavel, Hubert and Kerbrat, Alain and Mounier, Laurent and Mateescu, Radu and Sighireanu, Mihaela},
	booktitle={International Conference on Computer Aided Verification},
	pages={437--440},
	year={1996},
	organization={Springer}
}
@TechReport{Altarica2.3,
  author = 	 {Antoine B. Rauzy},
  title = 	 {Alta{R}ica {D}ataflow Language Specification  Version 2.3},
  institution =  {Ecole Centrale de Paris},
  year = 	 {2013},
 month = 	 {June}
}

@InProceedings{epoch,
  author = 	 {Teichteil-K{\"o}nigbuch, Florent and Infantes, Guillaume and Seguin, Christel },
  title = 	 {{EPOCH} Probabilistic {M}odel-{C}hecking},
 booktitle = {{M}odel {B}ased {S}afety {A}ssessment workshop},
  year = 	 {2011},
  address = 	 {Toulouse, France}
}

@inproceedings{bittner2016,
  title={Automated synthesis of timed failure propagation graphs},
  author={Bittner, Benjamin and Bozzano, Marco and Cimatti, Alessandro},
  booktitle={Proc. Int. Joint Conf. of Artificial Intelligence (IJCAI-16)},
  pages={972--978},
  year={2016}
}

@article{bozzano2012,
  title={Symbolic {M}odel {C}hecking and safety assessment of {AltaRica} models},
  author={Bozzano, Marco and Cimatti, Alessandro and Lisagor, Oleg and Mattarei, Cristian and Mover, Sergio and Roveri, Marco and Tonetta, Stefano},
  journal={Electronic Communications of the EASST},
  volume={46},
  year={2012}
}

@article{berthomieu1991TPN,
	title={Modeling and verification of time dependent systems using time {P}etri nets},
	author={Berthomieu, Bernard and Diaz, Michel},
	journal={IEEE transactions on software engineering},
	volume={17},
	number={3},
	pages={259--273},
	year={1991},
	publisher={IEEE}
}

@inproceedings{Zalila,
	author = {Zalila, F. and  Jenn, É. and Pantel, M. },
	title = {Model Execution and Debugging - A Process to Leverage Existing Tools},
	booktitle = { 5th International Conference on Model-Driven Engineering and Software Development},
	year = {2017}
}


@incollection{synoptic,
	author = {A. Cortier and L. Besnard and J. P. Bodeveix and J. Buisson and F. Dagnat and M. Filali and G. Garcia and J. Ouy and M. Pantel and A.-E. Rugina and M. Strecker and J.P. Talpin},
	title = {Synoptic: A Domain-Specific Modeling Language for Space On-board Application Software},
	booktitle = {Synthesis of Embedded Software},
	date = {2010}
}

@manual{sutre09,
	author = { Sutre , G. and Herbreteau, F. and  Fleury, F.},
	title = {Traduction de Synoptic en {AltaRica}},
	year = {2009},
	organization = {LaBRI}
}

@article{merlin1976,
	title={Recoverability of communication protocols--implications of a theoretical study},
	author={Merlin, Philip and Farber, David},
	journal={IEEE transactions on Communications},
	volume={24},
	number={9},
	pages={1036--1043},
	year={1976},
	publisher={IEEE}
}

@article{yao,
	title={A {P}etri net model for temporal knowledge representation and reasoning},
	author={Yao, Yulin},
	journal={IEEE Transactions on Systems, Man, and Cybernetics},
	volume={24},
	number={9},
	pages={1374--1382},
	year={1994},
	publisher={IEEE}
}


@book{ECSS‐E‐ST‐70‐11C,
	title = {Space segment operability},
	month = {31 July },
	year={2008},
	number = {ECSS-E-ST-70-11C}
}


@book{ECSS-E-ST-60-30C,
	title = {Satellite attitude and orbit control system ({AOCS}) requirements},
	month ={30 August },
	year={2013},
	number = {ECSS-E-ST-60-30C}
}

@book{ASRA,
title={Avionics {S}ystem {R}eference {A}rchitecture ({ASRA})},
publisher={ESA contract {4 000 102 927}}
}