Document Open Access Logo

An Approach to Formally Specifying the Behaviour of Mixed-Criticality Systems

Authors A. Burns, Cliff B. Jones

PDF
Thumbnail PDF

File

LIPIcs.ECRTS.2022.14.pdf
  • Filesize: 0.63 MB
  • 23 pages

Document Identifiers

Author Details

A. Burns
  • University of York, UK
Cliff B. Jones
  • Newcastle University, Newcastle upon Tyne, UK

Funding

This research has been supported in part by EPSRC (UK) grants, STRATA and MCCps and by Leverhulme Trust grant RPG-2019-020.

Acknowledgements

The authors acknowledge useful suggestions made by Iain Bate, Sanjoy Baruah and Ian Hayes.

Cite AsGet BibTex

A. Burns and Cliff B. Jones. An Approach to Formally Specifying the Behaviour of Mixed-Criticality Systems. In 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 231, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECRTS.2022.14

Abstract

This paper proposes a formal framework for describing the relationship between a criticality-aware scheduler and a set of application tasks that are assigned different criticality levels. The exposition employs a series of examples starting with scheduling simple jobs and then moving on to mixed-criticality robust and resilient tasks. The proposed formalism extends the rely-guarantee approach, which facilitates formal reasoning about the functional behaviour of concurrent systems, to address real-time properties.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Embedded and cyber-physical systems
  • Software and its engineering → Real-time schedulability
Keywords
  • real-time
  • scheduling
  • mixed criticality
  • rely/guaranteed conditions

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. J.-R. Abrial. The B-Book: Assigning programs to meanings. Cambridge University Press, 1996. Google Scholar
  2. J.-R. Abrial. The Event-B Book. Cambridge University Press, Cambridge, UK, 2010. Google Scholar
  3. J. Baik and K. Kang. Schedulability analysis for task migration under multiple mixed-criticality systems. In Proc Korean Society of Computer Science, page X, 2019. Google Scholar
  4. S. K. Baruah, A. Burns, and Z. Guo. Scheduling mixed-criticality systems to guarantee some service under all non-erroneous behaviours. In Proc. ECRTS, pages 131-140, 2016. Google Scholar
  5. S.K. Baruah, V. Bonifaci, G. D'Angelo, A. Marchetti-Spaccamela, S. van der Ster, and L. Stougie. Mixed-criticality scheduling of sporadic task systems. In Proc. of the 19th Annual European Symposium on Algorithms (ESA 2011) LNCS 6942, Saarbruecken, Germany, pages 555-566, 2011. Google Scholar
  6. S.K. Baruah, A. Burns, and R.I. Davis. Response-time analysis for mixed criticality systems. In Proc. IEEE Real-Time Systems Symposium (RTSS), pages 34-43, 2011. Google Scholar
  7. I. Bate, A. Burns, and R.I. Davis. An enhanced bailout protocol for mixed criticality embedded software. IEEE Transactions on Software Engineering, 43(4):298-320, 2016. Google Scholar
  8. I. Bate, A. Burns, and R.I. Davis. Analysis-runtime co-design for adaptive mixed criticality scheduling. In Proc. of forthcoming IEEE RTAS, Pre publication version privately communicated., 2022. Google Scholar
  9. R. Bornat and H. Amjad. Explanation of two non-blocking shared-variable communication algorithms. Formal Aspects of Computing, 25(6):893-931, 2013. Google Scholar
  10. S. Bozhko and B.B. Brandenburg. Abstract response-time analysis: A formal foundation for the busy-window principle. In Marcus Völp, editor, 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020), volume 165 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:24, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Google Scholar
  11. A. Burns. Why the expressive power of programming languages such as Ada is needed for future cyber physical systems. In Ada-Europe International Conference on Reliable Software Technologies, pages 3-11. Springer, 2016. Google Scholar
  12. A. Burns, S. Baruah, C.B. Jones, and I. Bate. Reasoning about the relationship between the scheduler and mixed-criticality jobs. In Proc. 7th Int. RTSS Workshop On Mixed Criticality Systems (WMC), pages 17-22, 2019. Google Scholar
  13. A. Burns and S.K. Baruah. Towards a more practical model for mixed criticality systems. In Proc. 1st Workshop on Mixed Criticality Systems (WMC), RTSS, pages 1-6, 2013. Google Scholar
  14. A. Burns, R. Davis, S. K. Baruah, and I. Bate. Robust mixed-criticality systems. IEEE Transactions on Computers, 67(10):1478-1491, 2018. Google Scholar
  15. A. Burns and R.I. Davis. Response-time analysis for mixed-criticality systems with arbitrary deadlines. In Proc. Workshop on Mixed Criticality Systems (WMC), pages 13-18, 2017. Google Scholar
  16. A. Burns and R.I. Davis. A survey of research into mixed criticality systems. ACM Computer Surveys, 50(6):1-37, 2017. Google Scholar
  17. A. Burns and R.I. Davis. Mixed criticality systems: A review (13th edition). Technical Report MCC-1(13), available at https://www-users.cs.york.ac.uk/~burns/review.pdf and the White Rose Repository, Department of Computer Science, University of York, 2022.
  18. A. Burns and I.J. Hayes. A timeband framework for modelling real-time systems. Real-Time Systems Journal, 45(1-2):106-142, June 2010. Google Scholar
  19. A. Burns, I.J. Hayes, and C.B. Jones. Deriving specifications of control programs for cyber physical systems. Computer Journal, 63(5):774-790, 2020. Google Scholar
  20. G. Buttazzo, G. Lipari, and L. Abeni. Elastic task model for adaptive rate control. In IEEE Real-Time Systems Symposium, pages 286-295, 1998. Google Scholar
  21. F. Cerqueira, F. Stutz, and B.B. Brandenburg. PROSA: A case for readable mechanized schedulability analysis. In Proc. 28th Euromicro Conference on Real-Time Systems (ECRTS), Leibniz International Proceedings in Informatics (LIPIcs), pages 273-284, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Google Scholar
  22. Diego Machado Dias. Mechanising an algebraic rely-guarantee refinement calculus. PhD thesis, School of Computing, Newcastle University, 2017. Google Scholar
  23. T. Fleming and A. Burns. Incorporating the notion of importance into mixed criticality systems. In L. Cucu-Grosjean and R. Davis, editors, Proc. 2nd Workshop on Mixed Criticality Systems (WMC), RTSS, pages 33-38, 2014. Google Scholar
  24. O. Gettings, S. Quinton, and R.I. Davis. Mixed criticality systems with weakly-hard constraints. In Proc. International Conference on Real-Time Networks and Systems (RTNS)), pages 237-246, 2015. Google Scholar
  25. C. Gill, J. Orr, and S. Harris. Supporting graceful degradation through elasticity in mixed-criticality federated scheduling. In Jing Li and Zhishan Guo, editors, Proc. 6th Workshop on Mixed Criticality Systems (WMC), RTSS, pages 19-24, 2018. Google Scholar
  26. X. Gu and A. Easwaran. Dynamic budget management with service guarantees for mixed-criticality systems. In Proc. Real-Time Systems Symposium (RTSS), pages 47-56. IEEE, 2016. Google Scholar
  27. X. Gu and A. Easwaran. Dynamic budget management and budget reclamation for mixed-criticality systems. Real-Time Systems, 55:552-597, 2019. Google Scholar
  28. X. Gu, K.-M. Phan, A. Easwaran, and I. Shin. Resource efficient isolation mechanisms in mixed-criticality scheduling. In Proc. 27th ECRTS, pages 13-24. IEEE, 2015. Google Scholar
  29. I. J. Hayes. Generalised rely-guarantee concurrency: An algebraic foundation. Formal Aspects of Computing, 28(6):1057-1078, November 2016. Google Scholar
  30. I.J. Hayes, M. Jackson, and C.B. Jones. Determining the specification of a control system from that of its environment. In Keijiro Araki, Stefani Gnesi, and Dino Mandrioli, editors, FME 2003: Formal Methods, volume 2805 of LNCS, pages 154-169. Springer Verlag, 2003. Google Scholar
  31. I.J. Hayes and C.B. Jones. A guide to rely/guarantee thinking. In Jonathan Bowen, Zhiming Liu, and Zili Zhan, editors, Engineering Trustworthy Software Systems - Third International School, SETSS 2017, volume 11174 of LNCS, pages 1-38. Springer, 2018. Google Scholar
  32. C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580, 1969. Google Scholar
  33. L. Huang, I-H. Hou, S.S. Sapatnekar, and J. Hu. Graceful degradation of low-criticality tasks in multiprocessor dual-criticality systems. In Proc. of the 26th International Conference on Real-Time Networks and Systems, RTNS, pages 159-169. ACM, 2018. Google Scholar
  34. P. Huang, P. Kumar, N. Stoimenov, and L. Thiele. Interference constraint graph: A new specification for mixed-criticality systems. In Proc. 18th Emerging Technologies and Factory Automation (ETFA), pages 1-8. IEEE, 2013. Google Scholar
  35. S. Iacovelli, R. Kirner, and C. Menon. ATMP: An adaptive tolerance-based mixed-criticality protocol for multi-core systems. In Proc. IEEE 13th International Symposium on Industrial Embedded Systems (SIES), pages 1-9, 2018. Google Scholar
  36. M. Jan, L. Zaourar, and M. Pitel. Maximizing the execution rate of low criticality tasks in mixed criticality system. In Proc. 1st WMC, RTSS, pages 43-48, 2013. Google Scholar
  37. C.B. Jones. Development Methods for Computer Programs including a Notion of Interference. PhD thesis, Oxford University, June 1981. Printed as: Programming Research Group, Technical Monograph 25. Google Scholar
  38. C.B. Jones. Specification and design of (parallel) programs. In Proc. of IFIP, pages 321-332. North-Holland, 1983. Google Scholar
  39. C.B. Jones. Systematic Software Development using VDM. Prentice Hall International, second edition, 1990. URL: http://homepages.cs.ncl.ac.uk/cliff.jones/ftp-stuff/Jones1990.pdf.
  40. C.B. Jones and A. Burns. A rely-guarantee specification of mixed-criticality scheduling. In Valentin Cassano and Nazareno Aguirre, editors, Mathematical Foundations of Software Engineering: Essays in Honor of Tom Maibaum on the Occasion of his Retirement, Tribute Series. College Publications, 2022. Google Scholar
  41. C.B. Jones and I.J. Hayes. Possible values: Exploring a concept for concurrency. Journal of Logical and Algebraic Methods in Programming, 85(5):972-984, 2016. Google Scholar
  42. C.B. Jones, I.J. Hayes, and M.A. Jackson. Deriving specifications for systems that are connected to the physical world. In Cliff B. Jones, Zhiming Liu, and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of Lecture Notes in Computer Science, pages 364-390. Springer Verlag, 2007. Google Scholar
  43. C.B. Jones and K.G. Pierce. Elucidating concurrent algorithms via layers of abstraction and reification. Formal Aspects of Computing, 23(3):289-306, 2011. Google Scholar
  44. C.B. Jones and N. Yatapanage. Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example. Formal Aspects of Computing, 31(3):353-374, 2019. on-line April 2018. Google Scholar
  45. J.C. Laprie. Dependable computing and fault tolerance: Concepts and terminology. In Digest of Papers, The Fifteenth Annual International Symposium on Fault-Tolerant Computing, pages 2-11, Michigan, USA, 1985. Google Scholar
  46. J. Lee, H.S. Chwa, L.T.X. Phan, I. Shin, and I. Lee. MC-ADAPT: Adaptive task dropping in mixed-criticality scheduling. ACM Trans. Embed. Comput. Syst., 16:163:1-163:21, 2017. Google Scholar
  47. J. Lee and J. Lee. Mc-flex: Flexible mixed-criticality real-time scheduling by task-level mode switch. IEEE Transactions on Computers, page online, 2021. URL: https://doi.org/10.1109/TC.2021.3111743.
  48. Hongjin Liang, Xinyu Feng, and Ming Fu. A rely-guarantee-based simulation for verifying concurrent program transformations. In Proc. 39th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '12, pages 455-468, New York, NY, USA, 2012. Google Scholar
  49. D. Liu, N. Guan, J. Spasic, G. Chen, S. Liu, T. Stefanov, and W. Yi. Scheduling analysis of imprecise mixed-criticality real-time tasks. IEEE Transactions on Computers, 67(7):975-991, July 2018. Google Scholar
  50. D. Liu, J. Spasic, N. Guan, G. Chen, S. Liu, T. Stefanov, and W. Yi. EDF-VD scheduling of mixed-criticality systems with degraded quality guarantees. In Proc. IEEE RTSS, pages 35-46, 2016. Google Scholar
  51. R. Medina, E. Borde, and L. Pautet. Directed acyclic graph scheduling for mixed-criticality systems. In Johann Blieberger and Markus Bader, editors, Reliable Software Technologies - Ada-Europe, pages 217-232. Springer International Publishing, 2017. Google Scholar
  52. R.M. Pathan. Improving the quality-of-service for scheduling mixed-criticality systems on multiprocessors. In Marko Bertogna, editor, Proc. Euromicro Conference on Real-Time Systems (ECRTS), volume 76 of Leibniz International Proc. in Informatics (LIPIcs), pages 19:1-19:22. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  53. S. Ramanathan, A. Easwaran, and H. Cho. Multi-rate fluid scheduling of mixed-criticality systems on multiprocessors. Real-Time Systems, 54:247-277, 2018. Google Scholar
  54. B. Randell, J-C. Laprie, H. Kopetz, and B. Littlewood(Eds.). Predictably Dependable Computing Systems. Springer, 1995. Google Scholar
  55. B. Randell, P.A. Lee, and P.C. Treleaven. Reliability issues in computing system design. ACM Computing Surveys, 10(2):123-165, 1978. Google Scholar
  56. J. Ren and L.T.X. Phan. Mixed-criticality scheduling on multiprocessors using task grouping. In Proc. 27th ECRTS, pages 25-36. IEEE, 2015. Google Scholar
  57. H. Su, P. Deng, D. Zhu, and Q. Zhu. Fixed-priority dual-rate mixed-criticality systems: Schedulability analysis and performance optimization. In Proc. Embedded and Real-Time Computing Systems and Applications (RTCSA), pages 59-68. IEEE, 2016. Google Scholar
  58. H. Su, N. Guan, and D. Zhu. Service guarantee exploration for mixed-criticality systems. In Proc. Embedded and Real-Time Computing Systems and Applications (RTCSA), pages 1-10. IEEE, 2014. Google Scholar
  59. H. Su and D. Zhu. An elastic mixed-criticality task model and its scheduling algorithm. In Proc. of the Conference on Design, Automation and Test in Europe, DATE, pages 147-152, 2013. Google Scholar
  60. H. Su, D. Zhu, and D. Mosse. Scheduling algorithms for elastic mixed-criticality tasks in multicore systems. In Proc. RTCSA, 2013. Google Scholar
  61. S. Vestal. Preemptive scheduling of multi-criticality systems with varying degrees of execution time assurance. In Proc. Real-Time Systems Symposium (RTSS), pages 239-243, 2007. Google Scholar
  62. N. Vreman, A. Cervin, and M. Maggio. Stability and Performance Analysis of Control Systems Subject to Bursts of Deadline Misses. In Björn B. Brandenburg, editor, Proc. Euromicro Conference on Real-Time Systems (ECRTS), volume 196 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1-15:23, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Google Scholar
  63. H. Xu and A. Burns. Semi-partitioned model for dual-core mixed criticality system. In 23rd International Conference on Real-Time Networks and Systems (RTNS 2015), pages 257-266, 2015. Google Scholar
  64. H. Xu and A. Burns. A semi-partitioned model for mixed criticality systems. Journal of Systems and Software, 150:51-63, 2019. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact