The material has been transfered to Uppaal models repository:

The material below is obsolete.

Herschel-Planck Software Schedulability Analysis Using UPPAAL

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},
}

 Name                      Last modified      Size  Description
 Parent Directory                               -   
 HEADER.html               2021-10-06 10:36  3.6K  Description header of this directory.
 schedulability4.xml       2015-10-28 16:28   22K  ISoLA12: Uppaal SMC model of a running example.
 ISoLA2012-talk.pdf        2013-04-14 17:28  548K  ISoLA12 Presentation slides from the conference.
 ICTSS2012-tutorial.pdf    2012-11-19 05:46  568K  ICTSS12 Uppaal SMC tutorial part about schedulability analysis.
 ISoLA2012.pdf             2012-11-16 21:52  220K  ISoLA12 Publication draft on symbolic and statistical model checking.
 Herschel-SMC2.xml         2012-11-16 21:45   55K  ISoLA12: Uppaal SMC model of a Herschel setup.
 Herschel-SMC2.q           2012-11-16 21:45  3.2K  ISoLA12: Uppaal SMC query file for a Herschel model.
 schedulability4.q         2012-05-21 13:40  2.7K  ISoLA12: Uppaal SMC query file for a running example.
 QMchapter.pdf             2011-06-09 11:48  136K  Quasimodo: Chapter for industrial handbook including follow-up results where BCET is relaxed.
 HerschelNonDet-14.xtr.zip 2011-06-09 11:48  1.6M  Quasimodo: Uppaal 4.1 trace leading to an error in the model where BCET is 14% lower than WCET (98MB).
 HerschelNonDet-14.xml     2011-06-09 11:34   55K  Quasimodo: Uppaal 4.1 model where BCET is 14% lower than WCET (without limits) -- possible error found.
 HerschelNonDet-14-16.xml  2011-06-09 11:34   55K  Quasimodo: Uppaal 4.1 model where BCET is 14% lower than WCET (limited to 16 periods) -- no errors found.
 HerschelNonDet-10-16.xml  2011-06-09 11:27   55K  Quasimodo: model where BCET is 10% lower than WCET (limited to 16 periods).
 HerschelNonDet-10.xml     2011-06-09 11:26   55K  Quasimodo: Uppaal 4.1 model where BCET is 10% lower than WCET (without limits) -- no errors found.
 ISoLA2010.pdf             2010-12-12 12:00  234K  ISoLA10 Publication draft documenting the problem, the model and the results.
 ISoLA2010-talk.pdf        2010-10-22 12:35  531K  ISoLA10 Slides from conference presentation.
 HerschelEvents2.xml       2010-10-12 21:11   63K  ISoLA10 Uppaal 4.1 model of the tasks with purpose of scheduling analysis
 HerschelEvents2spor.xml   2010-08-18 14:08   64K  Attempt at modeling sporadic tasks literally (failed)
 HerschelEvents2.q         2010-06-09 13:41  1.4K  ISoLA10 Uppaal 4.1 queries for checking various properties
 gantt-2c.pdf              2010-05-17 11:29   96K  ISoLA10 Uppaal TIGA Gantt chart of the first two cycles of the system (compressed).
 gantt-2c.eps              2010-05-17 11:29  1.1M  ISoLA10 Uppaal TIGA Gantt chart of the first two cycles of the system (vectors).
 gantt-2c-5307x792.png     2010-05-17 11:29  131K  ISoLA10 Uppaal TIGA Gantt chart of the first two cycles of the system (bitmap).
 gantt-1c.pdf              2010-05-17 11:29   64K  ISoLA10 Uppaal TIGA Gantt chart of the first cycle of the system (compressed).
 gantt-1c.eps              2010-05-17 11:29  643K  ISoLA10 Uppaal TIGA Gantt chart of the first cycle of the system (vectors).
 gantt-1c-12943x792.png    2010-05-17 11:29  163K  ISoLA10 Uppaal TIGA Gantt chart of the first cycle of the system (bitmap).
 results.ods               2010-05-15 04:21   48K  ISoLA10 Final results in a spreadsheet (Open Document Format)
 herschel2.txt             2010-05-15 02:17  3.4K  ISoLA10 WCRT estimates from the model for various cycle limits
 herschel.txt              2010-05-15 02:17   13K  ISoLA10 WCRT estimates from the model for various cycle limits
 README.html               2010-01-01 12:00  287   Description footer of this directory.

Prepared by
Marius Mikučionis <marius@cs.aau.dk>