The material below is obsolete.
This directory contains documents from Terma's case study about
Herschel-Planck dual satellite mission by European Space Agency:
ISoLA2012.pdf
Publication documenting application of combined symbolic and statistical model checking.
See also slides from the ISoLA 2012 presentation talk and ICTSS 2012 tutorial.
ISoLA2010.pdf
Publication documenting the problem, the model and the results.
See also slides from the ISoLA 2010 presentation talk.
BibTex citations:
@incollection {sched12,
author = {David, Alexandre and Larsen, Kim and Legay, Axel and Miku\v{c}ionis, Marius},
affiliation = {Computer Science, Aalborg University, Denmark},
title = {Schedulability of Herschel-Planck Revisited Using Statistical Model Checking},
booktitle = {Leveraging Applications of Formal Methods, Verification and Validation.
Applications and Case Studies},
series = {Lecture Notes in Computer Science},
editor = {Margaria, Tiziana and Steffen, Bernhard},
publisher = {Springer Berlin / Heidelberg},
isbn = {978-3-642-34031-4},
keyword = {Computer Science},
pages = {293-307},
volume = {7610},
url = {http://dx.doi.org/10.1007/978-3-642-34032-1_28},
doi = {978-3-642-34032-1\_28}
note = {10.1007/978-3-642-34032-1_28},
year = {2012}
}
@inproceedings{sched10,
author = {Miku\v{c}ionis, Marius and Larsen, Kim Guldstrand and Rasmussen, Jacob Illum and Nielsen, Brian
and Skou, Arne and Palm, Steen Ulrik and Pedersen, Jan Storbank and Hougaard, Poul},
title = {Schedulability analysis using Uppaal: Herschel-Planck case study},
booktitle = {Proceedings of the 4th international conference on Leveraging applications of formal methods,
verification, and validation - Volume Part II},
series = {ISoLA'10},
year = {2010},
isbn = {3-642-16560-5, 978-3-642-16560-3},
location = {Heraklion, Crete, Greece},
pages = {175--190},
numpages = {16},
url = {http://portal.acm.org/citation.cfm?id=1939345.1939369},
acmid = {1939369},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
keywords = {model-checking, schedulability analysis, stop-watch automata, timed automata, verification},
}