Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

High-level frameworks for the specification and verification of scheduling problems

  • FMICS-AVoCS
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Over the years, schedulability of Cyber-Physical Systems (CPS) has mainly been performed by analytical methods. These techniques are known to be effective but limited to a few classes of scheduling policies. In a series of recent work, we have shown that schedulability analysis of CPS could be performed with a model-based approach and extensions of verification tools such as UPPAAL. One of our main contributions has been to show that such models are flexible enough to embed various types of scheduling policies, which goes beyond those in the scope of analytical tools. However, the specification of scheduling problems with model-based approaches requires a substantial modeling effort, and a deep understanding of the techniques employed in order to understand their results. In this paper we propose simplicity-driven high-level specification and verification frameworks for various scheduling problems. These frameworks consist of graphical and user-friendly languages for describing scheduling problems. The high-level specifications are then automatically translated to formal models, and results are transformed back into the comprehensible model view. To construct these frameworks we exploit a meta-modeling approach based on the tool generator Cinco . Additionally we propose in this paper two new techniques for scheduling analysis. The first performs runtime monitoring using the CUSUM algorithm to detect alarming change in the system. The second performs optimization using efficient statistical techniques. We illustrate our frameworks and techniques on two case studies.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17
Fig. 18
Fig. 19
Fig. 20
Fig. 21

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. http://cinco.scce.info/applications/.

  2. http://cinco.scce.info.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994). doi:10.1016/0304-3975(94)90010-8

    Article  MathSciNet  MATH  Google Scholar 

  2. Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. Theor. Comput. Sci. 318(3), 297–322 (2004). doi:10.1016/j.tcs.2003.10.038

    Article  MathSciNet  MATH  Google Scholar 

  3. Basseville, M., Nikiforov, I.V.: Detection of Abrupt Changes: Theory and Application. Prentice-Hall Inc, Englewood Cliffs (1993)

    Google Scholar 

  4. Beauquier, D.: On probabilistic timed automata. Theor. Comput. Sci. 292(1), 65–84 (2003). doi:10.1016/S0304-3975(01)00215-8

    Article  MathSciNet  MATH  Google Scholar 

  5. Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: Third International Conference on the Quantitative Evaluation of Systems (QEST), pp. 125–126 (2006). doi:10.1109/QEST.2006.59

  6. Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control (HSCC), pp. 147–161. Springer (2001). doi:10.1007/3-540-45351-2_15

  7. Boudjadar, A., David, A., Kim, J.H., Larsen, K.G., Mikuionis, M., Nyman, U., Skou, A.: Hierarchical scheduling framework based on compositional analysis using Uppaal. In: Proceedings of the 10th International Symposium on Formal Aspects of Component Software (FACS), Revised Selected Papers, LNCS, vol. 8348, pp. 61–78. Springer (2013). doi:10.1007/978-3-319-07602-7_6

  8. Boudjadar, A., David, A., Kim, J.H., Larsen, K.G., Mikuionis, M., Nyman, U., Skou, A.: Widening the schedulability of hierarchical scheduling systems. In: Proceedings of the 11th International Symposium on Formal Aspects of Component Software (FACS), Revised Selected Papers, LNCS, vol. 8997, pp. 209–227. Springer (2015). doi:10.1007/978-3-319-15317-9_14

  9. Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: Proceedings of the 11th International Conference on Concurrency Theory (CONCUR), pp. 138–152. Springer (2000). doi:10.1007/3-540-44618-4_12

  10. Cesta, A., Fratini, S., Orlandini, A., Finzi, A., Tronci, E.: Flexible plan verification: feasibility results. Fundam. Inform. 107(2–3), 111–137 (2011). doi:10.3233/FI-2011-397

    MathSciNet  MATH  Google Scholar 

  11. Chadli, M., Kim, J.H., Legay, A., Traonouez, L., Naujokat, S., Steffen, B., Larsen, K.G.: A model-based framework for the specification and analysis of hierarchical scheduling systems. In: Proceedings of the Joint 21st International Workshop on Formal Methods for Industrial Critical Systems and 16th International Workshop on Automated Verification of Critical Systems (FMICS-AVoCS), LNCS, vol. 9933, pp. 133–141. Springer (2016). doi:10.1007/978-3-319-45943-1_9

  12. Cimatti, A., Micheli, A., Roveri, M.: Dynamic controllability of disjunctive temporal networks: validation and synthesis of executable strategies. In: Proceedings of the 30th AAAI Conference on Artificial Intelligence, pp. 3116–3122. AAAI Press (2016)

  13. Cimatti, A., Micheli, A., Roveri, M.: Validating domains and plans for temporal planning via encoding into infinite-state linear temporal logic. In: Proceedings of the 31st AAAI Conference on Artificial Intelligence, pp. 3547–3554. AAAI Press (2017)

  14. David, A., Du, D., Larsen, K.G., Legay, A., Mikučionis, M.: Optimizing control strategy using statistical model checking. In: NASA Formal Methods: Proceedings of the 5th International Symposium (NFM), pp. 352–367. Springer (2013). doi:10.1007/978-3-642-38088-4_24

  15. David, A., Du, D., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for stochastic hybrid systems. In: Proceedings of the First International Workshop on Hybrid Systems and Biology (HSB), EPTCS, vol. 92, pp. 122–136 (2012). doi:10.4204/EPTCS.92.9

  16. David, A., Larsen, K.G., Legay, A., Mikucionis, M.: Schedulability of herschel-planck revisited using statistical model checking. In: Proceedings of 5th International Symposium ISoLA, Part II, LNCS, vol. 7610, pp. 293–307. Springer (2012). doi:10.1007/978-3-642-34032-1_28

  17. David, A., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Proceedings of the 9th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), LNCS, vol. 6919, pp. 80–96. Springer (2011). doi:10.1007/978-3-642-24310-3_7

  18. David, A., Larsen, K.G., Legay, A., Mikuionis, M., Poulsen, D.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. (2015). doi:10.1007/s10009-014-0361-y

    Google Scholar 

  19. David, A., Larsen, K.G., Legay, A., Poulsen, D.B.: Statistical model checking of dynamic networks of stochastic hybrid automata. ECEASST 66, 1–15 (2013)

    Google Scholar 

  20. David, A., Rasmussen, J.I., Larsen, K.G., Skou, A.: Model-based Framework for Schedulability Analysis Using Uppaal 4.1d. CRC Press LLC, Boca Raton (2009)

    Google Scholar 

  21. Gronback, R.C.: Eclipse Modeling Project: A Domain-Specific Language (DSL) Toolkit. Addison-Wesley, Boston (2008)

    Google Scholar 

  22. Henzinger, T.A.: The theory of hybrid automata, pp. 265–292. Springer (2000). doi:10.1007/978-3-642-59615-5_13

  23. Jrges, S., Lamprecht, A.L., Margaria, T., Schaefer, I., Steffen, B.: A constraint-based variability modeling framework. Int. J. Softw. Tools Technol. Transf. (STTT) 14(5), 511–530 (2012). doi:10.1007/s10009-012-0254-x

    Article  Google Scholar 

  24. Kim, J.H., Boudjadar, A., Nyman, U., Mikucionis, M., Larsen, K.G., Lee, I.: Quantitative schedulability analysis of continuous probability tasks in a hierarchical context. In: 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering (CBSE), pp. 91–100 (2015). doi:10.1145/2737166.2737170

  25. Kim, J.H., Legay, A., Larsen, K.G., Mikučionis, M., Nielsen, B.: Resource-parameterized timing analysis of real-time systems. In: Hardware and Software: Verification and Testing: Proceeding of the 11th International Haifa Verification Conference (HVC), pp. 190–205. Springer (2015). doi:10.1007/978-3-319-26287-1_12

  26. Kim, J.H., Legay, A., Traonouez, L.M., Boudjadar, A., Nyman, U., Larsen, K.G., Lee, I., Choi, J.Y.: Optimizing the resource requirements of hierarchical scheduling systems. SIGBED Rev. 13(3), 41–48 (2016). doi:10.1145/2983185.2983192

    Article  Google Scholar 

  27. Lamprecht, A.L., Naujokat, S., Schaefer, I.: Variability management beyond feature models. Computer 46(11), 48–54 (2013). doi:10.1109/MC.2013.299

    Article  Google Scholar 

  28. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Proceedings of the First International Conference on Runtime Verification (RV), LNCS, vol. 6418, pp. 122–135. Springer (2010). doi:10.1007/978-3-642-16612-9_11

  29. Legay, A., Traonouez, L.M.: Statistical model checking with change detection. Trans. Found. Mastering Change I(1), 157–179 (2016). doi:10.1007/978-3-319-46508-1_9

    Article  Google Scholar 

  30. Locke, D., Lucas, L., Goodenough, J.: Generic avionics software specification. Tech. Rep. CMU/SEI-90-TR-008, Software Engineering Institute (1990)

  31. Margaria, T., Steffen, B.: business process modelling in the jABC: the one-thing-approach. In: Handbook of Research on Business Process Modeling. IGI Global (2009)

  32. Margaria, T., Steffen, B.: Simplicity as a driver for agile innovation. Computer 43(6), 90–92 (2010). doi:10.1109/MC.2010.177

    Article  Google Scholar 

  33. Montgomery, D.C.: Design and Analysis of Experiments. Wiley, Hoboken (2006)

    Google Scholar 

  34. Naujokat, S., Lybecait, M., Kopetzki, D., Steffen, B.: CINCO: A simplicity-driven approach to full generation of domain-specific graphical modeling tools. Softw. Tools Technol. Transf. (2017) (To appear)

  35. Naujokat, S., Traonouez, L.M., Isberner, M., Steffen, B., Legay, A.: Domain-specific code generator modeling: a case study for multi-faceted concurrent systems. In: Proceedings of the 6th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Part I (ISoLA), no. 8802 in LNCS, pp. 463–480. Springer (2014). doi:10.1007/978-3-662-45234-9_33

  36. Oddi, A., Rasconi, R., Cesta, A.: A multi-objective large neighborhood search methodology for scheduling problems with energy costs. In: 2015 IEEE 27th International Conference on Tools with Artificial Intelligence (ICTAI), pp. 453–460 (2015). doi:10.1109/ICTAI.2015.74

  37. Page, E.S.: Continuous inspection schemes. Biometrika 41(1/2), 100–115 (1954)

    Article  MathSciNet  MATH  Google Scholar 

  38. Phan, L.T.X., Lee, J., Easwaran, A., Ramaswamy, V., Chen, S., Lee, I., Sokolsky, O.: CARTS: a tool for compositional analysis of real-time systems. SIGBED Rev. 8(1), 62–63 (2011). doi:10.1145/1967021.1967029

    Article  Google Scholar 

  39. Shin, I., Easwaran, A., Lee, I.: Hierarchical scheduling framework for virtual clustering of multiprocessors. In: Euromicro Conference on Real-Time Systems, pp. 181–190 (2008). doi:10.1109/ECRTS.2008.28

  40. Shin, I., Lee, I.: Periodic resource model for compositional real-time guarantees. In: Proceedings of the 24th IEEE International Real-Time Systems Symposium (RTSS), pp. 2–13. IEEE Computer Society (2003)

  41. Smith, D., Frank, J., Cushing, W.: The anml language. In: In ICAPS Poster session (2008)

  42. Steinberg, D., Budinsky, F., Paternostro, M., Merks, E.: EMF: Eclipse Modeling Framework, 2nd edn. Addison-Wesley, Reading (2008)

    Google Scholar 

  43. Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117–186 (1945)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Irisa, Rennes, France

    Mounir Chadli

  2. University of Pennsylvania, Philadelphia, PA, USA

    Jin H. Kim

  3. Aalborg University, Ålborg, Denmark

    Kim G. Larsen

  4. Inria, Rennes, France

    Axel Legay & Louis-Marie Traonouez

  5. Technishe Universität Dortmund, Dortmund, Germany

    Stefan Naujokat & Bernhard Steffen

Authors
  1. Mounir Chadli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jin H. Kim
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Kim G. Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Stefan Naujokat
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Bernhard Steffen
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Louis-Marie Traonouez
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Louis-Marie Traonouez.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Chadli, M., Kim, J.H., Larsen, K.G. et al. High-level frameworks for the specification and verification of scheduling problems. Int J Softw Tools Technol Transfer 20, 397–422 (2018). https://doi.org/10.1007/s10009-017-0466-1

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-017-0466-1

Keywords

Search

Navigation