Parametric Schedulability Analysis of a Launcher Flight Control System under Reactivity Constraints.

• Autorzy: André Étienne , Coquard Emmanuel , Fribourg Laurent , Jerray Jawher , Lesens David , Keller Jörg , Penczek Wojciech

Identyfikatory

DOI

10.3233/FI-2021-2065

• Języki publikacji: EN

Abstrakty

EN

The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. In this paper, we present an approach for the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We first describe the problem of the scheduling of a launcher flight control, then we show how this problem can be formalized with parametric stopwatch automata; we then present the results computed by the parametric timed model checker IMITATOR. We enhance our model by taking into consideration the time for switching context, and we compare the results to those obtained by other tools classically used in scheduling.

Słowa kluczowe

EN

scheduling; real-time systems; model checking; parameter synthesis; IMITATOR

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 182, nr 1
• Strony: 31--67
• Opis fizyczny: Bibliogr. 59 poz., rys., tab.

Twórcy

autor

André Étienne

• Université de Lorraine, CNRS, Inria, LORIA, Nancy, France

autor

Coquard Emmanuel

• ArianeGroup SAS, Les Mureaux, France

autor

Fribourg Laurent

• Université Paris-Saclay, LSV, CNRS, ENS Paris-Saclay, France

autor

Jerray Jawher

• Université Sorbonne Paris-Nord, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France

autor

Lesens David

• ArianeGroup SAS, Les Mureaux, France

autor

Keller Jörg

autor

Penczek Wojciech

Bibliografia

• [1] Alur R, Dill DL. A theory of timed automata. Theoretical Computer Science, 1994. 126(2):183-235. doi:10.1016/0304-3975(94)90010-8.
• [2] Alur R, Henzinger TA, Vardi MY. Parametric real-time reasoning. In: Kosaraju SR, Johnson DS, Aggarwal A (eds.), STOC. ACM, New York, NY, USA, 1993 pp. 592-601. doi:10.1145/167088.167242.
• [3] Cassez F, Larsen KG. The Impressive Power of Stopwatches. In: Palamidessi C (ed.), CONCUR, volume 1877 of Lecture Notes in Computer Science. Springer, 2000 pp. 138-152. doi:10.1007/3-540-44618-4 12.
• [4] Sun Y, Soulat R, Lipari G, Andr´e ´E, Fribourg L. Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems. In: Artho C, ¨Olveczky P (eds.), FSTCS, volume 419 of Communications in Computer and Information Science. Springer, 2013 pp. 212-228. doi:10.1007/978-3-319-05416-2 14.
• [5] André E. IMITATOR 3: Synthesis of timing parameters beyond decidability. In: Leino R, Silva A (eds.), CAV. 2021 To appear.
• [6] Beneˇs N, Bezdˇek P, Larsen KG, Srba J. Language Emptiness of Continuous-Time Parametric Timed Automata. In: Halld´orsson MM, Iwama K, Kobayashi N, Speckmann B (eds.), ICALP, Part II, volume 9135 of Lecture Notes in Computer Science. Springer, 2015 pp. 69-81. doi:10.1007/978-3-662-47666-6_6.
• [7] Miller JS. Decidability and Complexity Results for Timed Automata and Semi-linear Hybrid Automata. In: Lynch NA, Krogh BH (eds.), HSCC, volume 1790 of Lecture Notes in Computer Science. Springer. ISBN 3-540-67259-1, 2000 pp. 296-309. doi:10.1007/3-540-46430-1 26
• [8] André E. What’s decidable about parametric timed automata? International Journal on Software Tools for Technology Transfer, 2019. 21(2):203-219. doi:10.1007/s10009-017-0467-0.
• [9] Hune T, Romijn J, Stoelinga M, Vaandrager FW. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming, 2002. 52-53:183-220. doi:10.1016/S1567-8326(02)00037-1.
• [10] Bozzelli L, La Torre S. Decision problems for lower/upper bound parametric timed automata. Formal Methods in System Design, 2009. 35(2):121-151. doi:10.1007/s10703-009-0074-0.
• [11] André E, Lime D. Liveness in L/U-Parametric Timed Automata. In: Legay A, Schneider K (eds.), ACSD. IEEE, 2017 pp. 9-18. doi:10.1109/ACSD.2017.19.
• [12] André E, Lime D, Ramparison M. TCTL model checking lower/upper-bound parametric timed automata without invariants. In: Jansen DN, Prabhakar P (eds.), FORMATS, volume 11022 of Lecture Notes in Computer Science. Springer, 2018 pp. 1-17. doi:10.1007/978-3-030-00151-33.
• [13] Cimatti A, Palopoli L, Ramadian Y. Symbolic Computation of Schedul ability Regions Using Parametric Timed Automata. In: RTSS. IEEE Computer Society. ISBN 978-0-7695-3477-0, 2008 pp. 80-89. doi: 10.1109/RTSS.2008.36.
• [14] André E. A unified formalism for mono processor schedule ability analysis under uncertainty. In: Cavalcanti A, Petrucci L, Seceleanu C (eds.), FMICS-AVoCS, volume 10471 of Lecture Notes in Computer Science. Springer, 2017 pp. 100-115. doi:10.1007/978-3-319-67113-07.
• [15] Chevallier R, Encrenaz-Tiph`ene E, Fribourg L, Xu W. Timed Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata. Formal Methods in System Design, 2009. 34(1):59-81. doi:10.1007/s10703-008-0061-x.
• [16] Fanchon L, Jacquemard F. Formal Timing Analysis Of Mixed Music Scores. In: ICMC. Michigan Publishing, 2013 .
• [17] André E, Hasuo I, Waga M. Offline timed pattern matching under uncertainty. In: Lin AW, Sun J (eds.), ICECCS. IEEE Computer Society, 2018 pp. 10-20. doi:10.1109/ICECCS2018.2018.00010.
• [18] Luthmann L, Gerecht T, Stephan A, B¨urdek J, Lochau M. Minimum/maximum delay testing of product lines with unbounded parametric real-time constraints. Journal of Systems and Software, 2019. 149:535-553. doi:10.1016/j.jss.2018.12.028.
• [19] Bate I, Burns A. Schedul ability analysis of fixed priority real-time systems with offsets. In: RTS. IEEE, 1997 pp. 153-160. doi:10.1109/EMWRTS.1997.613776.
• [20] Bini E, Buttazzo GC. Schedul ability Analysis of Periodic Fixed Priority Systems. IEEE Transactions on Computers, 2004. 53(11):1462-1473. doi:10.1109/TC.2004.103.
• [21] Wang F, Mok AK, Emerson EA. Formal Specification of Synchronous Distributed Real-Time Systems by APTL. In: Montgomery T, Clarke LA, Ghezzi C (eds.), ICSE. ACM Press, 1992 pp. 188-198. doi:10.1145/143062.143113.
• [22] Yang J, Mok AK, Wang F. Symbolic Model Checking for Event-Driven Real-Time Systems. ACM Transactions on Programming Languages and Systems, 1997. 19(2):386-412. doi:10.1145/244795.244803.
• [23] Campos SVA, Clarke EM. Analysis and Verification of Real-Time Systems Using Quantitative Symbolic Algorithms. International Journal on Software Tools for Technology Transfer, 1999. 2(3):260-269. doi:10.1007/s100090050033.
• [24] Abdedda¨ım Y, Maler O. Job-Shop Scheduling Using Timed Automata. In: Berry G, Comon H, Finkel A (eds.), CAV, volume 2102 of Lecture Notes in Computer Science. Springer. ISBN 3-540-42345-1, 2001 pp. 478-492. doi:10.1007/3-540-44585-4 46.
• [25] Adbedda¨ım Y, Maler O. Preemptive Job-Shop Scheduling using Stopwatch Automata. In: Katoen JP, Stevens P (eds.), TACAS, volume 2280 of Lecture Notes in Computer Science. Springer-Verlag, 2002 pp. 113-126. doi:10.1007/3-540-46002-09.
• [26] Adbedda¨ım Y, Asarin E, Maler O. Scheduling with timed automata. Theoretical Computer Science, 2006. 354(2):272-300. doi:10.1016/j.tcs.2005.11.018.
• [27] Norstr¨om C, Wall A, Yi W. Timed Automata as Task Models for Event-Driven Systems. In: RTCSA. IEEE Computer Society, 1999 pp. 182-189. doi:10.1109/RTCSA.1999.811218.
• [28] Fersman E, Krc´al P, Pettersson P, Yi W. Task automata: Schedul ability, decidability and undecidability. Information and Computation, 2007. 205(8):1149-1172. doi:10.1016/j.ic.2007.01.009.
• [29] Sun Y, Lipari G, Soulat R, Fribourg L, Markey N. Component-based analysis of hierarchical scheduling using linear hybrid automata. In: ERTCS. IEEE Computer Society, 2014 pp. 1–10. doi:10.1109/RTCSA. 2014.6910502.
• [30] Sun Y, Lipari G. A Weak Simulation Relation for Real-Time Schedul ability Analysis of Global Fixed Priority Scheduling Using Linear Hybrid Automata. In: Jan M, Hedia BB, Goossens J, Maiza C (eds.), RTNS. ACM, 2014 p. 35. doi:10.1145/2659787.2659814.
• [31] Fang B, Li G, Sun D, Cai H. Schedul ability Analysis of Timed Regular Tasks by Under-Approximation on WCET. In: Fr¨anzle M, Kapur D, Zhan N (eds.), SETTA, volume 9984 of Lecture Notes in Computer Science. 2016 pp. 147-162. doi:10.1007/978-3-319-47677-3 10.
• [32] Forget J, Boniol F, Grolleau E, Lesens D, Pagetti C. Scheduling Dependent Periodic Tasks without Synchronization Mechanisms. In: Caccamo M (ed.), RTAS. IEEE Computer Society, 2010 pp. 301-310. doi:10.1109/RTAS.2010.26.
• [33] Mikucionis M, Larsen KG, Rasmussen JI, Nielsen B, Skou A, Palm SU, Pedersen JS, Hougaard P. Schedul ability Analysis Using Uppaal: Herschel-Planck Case Study. In: Margaria T, Steffen B (eds.), ISoLA, Part II, volume 6416 of Lecture Notes in Computer Science. Springer, 2010 pp. 175-190. doi: 10.1007/978-3-642-16561-0 21.
• [34] Fribourg L, Lesens D, Moro P, Soulat R. Robustness Analysis for Scheduling Problems using the Inverse Method. In: Reynolds M, Terenziani P, Moszkowski B (eds.), TIME. IEEE Computer Society Press, 2012 pp. 73-80. doi:10.1109/TIME.2012.10.
• [35] André E, Chatain Th, Encrenaz E, Fribourg L. An Inverse Method for Parametric Timed Au-tomata. International Journal of Foundations of Computer Science, 2009. 20(5):819-836. doi:10.1142/S0129054109006905.
• [36] André E, Soulat R. The Inverse Method. FOCUS Series in Computer Engineering and Information Technology. ISTE Ltd and John Wiley & Sons Inc., 2013. ISBN 9781848214477.
• [37] Sun Y, Andr´e ´E, Lipari G. Verification of Two Real-Time Systems Using Parametric Timed Automata. In: Quinton S, Vardanega T (eds.), WATERS. 2015 .
• [38] André E, Fribourg L, Mota JM, Soulat R. Verification of an industrial asynchronous leader elec-tion algorithm using abstractions and parametric model checking. In: Enea C, Piskac R (eds.), VM-CAI, volume 11388 of Lecture Notes in Computer Science. Springer, 2019 pp. 409-424. doi:10.1007/978-3-030-11245-5 19.
• [39] Le TTH, Palopoli L, Passerone R, Ramadian Y. Timed-automata based schedulability analysis for distributed firm real-time systems: a case study. International Journal on Software Tools for Technology Transfer, 2013. 15(3):211-228. doi:10.1007/s10009-012-0245-y.
• [40] B´erard B, Haddad S, Jovanovic A, Lime D. Interrupt Timed Automata with Auxiliary Clocks and Parameters. Fundamenta Informormatica, 2016. 143(3-4):235-259. doi:10.3233/FI-2016-1313.
• [41] Lime D, Roux OH, Seidner C, Traonouez LM. Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. In: Kowalewski S, Philippou A (eds.), TACAS, volume 5505 of Lecture Notes in Computer Science. Springer, 2009 pp. 54-57. doi:10.1007/978-3-642-00768-2 6.
• [42] Traonouez LM, Lime D, Roux OH. Parametric Model-Checking of Stopwatch Petri Nets. Journal of
• Universal Computer Science, 2009. 15(17):3273-3304. doi:10.3217/jucs-015-17-3273.
• [43] Parquier B, Rioux L, Henia R, Soulat R, Roux OH, Lime D, Andr´e ´E. Applying parametric model-checking techniques for reusing real-time critical systems. In: Artho C, ¨Olveczky PC (eds.), FTSCS, volume 694 of Communications in Computer and Information Science. Springer, 2016 pp. 129-144. doi:10.1007/978-3-319-53946-1 8.
• [44] Ober I, Graf S, Lesens D. Modeling and Validation of a Software Architecture for the Ariane-5 Launcher. In: Gorrieri R, Wehrheim H (eds.), FMOODS, volume 4037 of Lecture Notes in Computer Science. Springer, 2006 pp. 48-62. doi:10.1007/11768869 6.
• [45] Ghoshhajra M, Nair S, Cm AC. ARINC 653 API and its application – An insight into Avionics System Case Study. Defence science journal, 2013. 63. doi:10.14429/dsj.63.4268.
• [46] Liu CL, Layland JW. Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment. Journal of the ACM, 1973. 20(1):46-61. doi:10.1145/321738.321743.
• [47] Jovanovi´c A, Lime D, Roux OH. Integer Parameter Synthesis for Real-Time Systems. IEEE Transactions on Software Engineering, 2015. 41(5):445-461. doi:10.1109/TSE.2014.2357445.
• [48] Aceto L, Bouyer P, Burgue˜no A, Larsen KG. The power of reachability testing for timed automata. Theoretical Computer Science, 2003. 300(1-3):411-475. doi:10.1016/S0304-3975(02)00334-1.
• [49] André E. Observer Patterns for Real-Time Systems. In: Liu Y, Martin A (eds.), ICECCS. IEEE Computer Society, 2013 pp. 125-134. doi:10.1109/ICECCS.2013.26.
• [50] Shin I, Lee I. Periodic Resource Model for Compositional Real-Time Guarantees. In: RTSS. IEEE Computer Society, 2003 pp. 2-13. doi:10.1109/REAL.2003.1253249.
• [51] Richter K. Compositional scheduling analysis using standard event models: The SymTA/S ap-proach. Ph.D. thesis, University of Braunschweig - Institute of Technology, 2005. doi:10.24355/dbbs.084-200511080100-362. URL http://d-nb.info/978460332.
• [52] Lipari G, Bini E. A methodology for designing hierarchical scheduling systems. Journal of Embedded Computing, 2005. 1(2):257-269. URL http://content.iospress.com/articles/journal-of-embedded-computing/jec00019.
• [53] Shin I, Easwaran A, Lee I. Hierarchical Scheduling Framework for Virtual Clustering of Multiprocessors. In: ECRTS. IEEE Computer Society, 2008 pp. 181-190. doi:10.1109/ECRTS.2008.28.
• [54] Carnevali L, Pinzuti A, Vicario E. Compositional Verification for Hierarchical Scheduling of Real-Time Systems. IEEE Transactions on Software Engineering, 2013. 39(5):638-657. doi:10.1109/TSE.2012.54.
• [55] Singhoff F. The Cheddar project: a GPL real-time scheduling analyzer. http://beru.univ-brest.fr/singhoff/cheddar/.
• [56] Larsen KG, Pettersson P, Yi W. UPPAAL in a Nutshell. International Journal on Software Tools for Technology Transfer, 1997. 1(1-2):134-152. doi:10.1007/s100090050010.
• [57] Bagnara R, Hill PM, Zaffanella E. The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems. Science of Computer Programming, 2008. 72(1-2):3-21. doi:10.1016/j.scico.2007.08.001.
• [58] Bini E, Buttazzo GC. Measuring the Performance of Schedul ability Tests. Real-Time Systems, 2005. 30(1-2):129-154. doi:10.1007/s11241-005-0507-9.
• [59] Emberson P, Stafford R, Davis RI. Techniques For The Synthesis Of Multiprocessor Tasksets. In: WA-TERS. 2010 pp. 6-11. URL http://retis.sssup.it/waters2010/waters2010.pdf

Uwagi

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023).