General model of real-time modular computer systems operation for checking acceptability of such systems configurations

A. B. Glonina

Vestnik Ûžno-Uralʹskogo gosudarstvennogo universiteta. Seriâ Vyčislitelʹnaâ matematika i informatika, Tome 6 (2017) no. 4, pp. 43-59

Résumé

In this paper, we consider schedulability analysis problem for real-time modular computer systems (RT MCS). A system configuration is called schedulable if all the jobs complete within their deadlines. The paper contains formal definitions of a system configuration and a system operation trace which is necessary for checking the schedulability criterion. The author proposes a stopwatch automata-based general model of RT MCS operation. A model instance for a given RT MCS configuration is a network of stopwatch automata and it can be built automatically using the general model. A system operation trace can be obtained from the corresponding NSA trace. The stopwatch automata formalism allowed us to prove that the model is deterministic and satisfies a set of correctness requirements derived from RT MCS specifications. We implemented our approach in software and compared it experimentally with Model Checking approach, which uses the same formalism. The results of the experiments confirm that our approach is much more efficient. The software implementation is also integrated with the existing industrial RT MCS scheduling tool. These experiments showed the applicability of the proposed approach to real scale systems.

Détail

Keywords: modular computer systems, schedulability analysis, stopwatch automata, real-time systems.
Mots-clés : simulation

Bibliographie

[1] K. Senthilkumar, R. Ramadoss, “Designing Multicore ECU Architecture in Vehicle Networks Using AUTOSAR”, ICoAC (Chennai, India, December 14–16, 2011), Proceedings of the Third International Conference on Advanced Computing, 270–275 | DOI

[2] From the Ground Up: How the Internet of Things Will Give Rise to Connected Aviation, Gogo LLC, 2016, 140 pp.

[3] S. Marinescu, D. Tamas-Selicean, V. Acretoaie et al., “Timing Analysis of Mixed-Criticality Hard Real-Time Applications Implemented on Distributed Partitioned Architectures”, ETFA (Krakow, Poland, September 17–21, 2012), Proceedings of the 17th IEEE International Conference on Emerging Technologies and Factory Automation, 1–4 | DOI

[4] G. Macariu, V. Cretu, “Timed Automata Model For Component-Based Real-Time Systems”, ECBS (Oxford, UK, March 22–26, 2010), Proceedings of the 17th IEEE International Conference and Workshops on Engineering of Computer Based Systems, 121–130 | DOI

[5] J. P. Craveiro, R. O. Silveira, J. Rufino, “HsSim: an Extensible Interoperable Object-Oriented n-Level Hierarchical Scheduling Simulator”, WATERS (Pisa, Italy, July 10, 2012), Proceedings of the 3rd International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems, 9–14

[6] F. Singhoff, A. Plantec, P. Dissaux et al., “Investigating the Usability of Real-Time Scheduling Theory with the Cheddar Project”, Real-Time Systems, 43:3 (2009), 259–295 | DOI

[7] A. Khoroshilov, D. Albitskiy, I. Koverninskiy et al., “AADL-Based Toolset for IMA System Design and Integration”, SAE Int. J. Aerosp, 5:2 (2012), 294–299 | DOI

[8] P. Dissaux, O. Marc, C. Fotsing et al., “The SMART project: Multi-Agent Scheduling Simulation Of Real-Time Architectures”, Embedded Real Time Software and Systems, 2014

[9] V. V. Balashov, V. A. Balakhanov, V. A. Kostenko, “Scheduling of Computational Tasks in Switched Network-Based IMA systems”, OPTI (Athens, Greece, June 4–6, 2014), Proceedings of International Conference on Engineering and Applied Sciences Optimization, 1001–1014

[10] F. Cassez, K. Larsen, “The Impressive Power of Stopwatches”, CONCUR 2000 — Concurrency Theory (PA, USA, August 22–25, 2000), LNCS, 1877, Springer, 138–152 | DOI

[11] A. Tretyakov, “Automation of Scheduling for Periodic Real-Time Systems”, Proceedings of the Institute for System Programming, 22 (2012), 375–400 | DOI

[12] R. L. Smelyansky, “Model of Distributed Computing System Operation With Time”, Programming and Computer Software, 39:5 (2013), 233–241 | DOI

[13] J. Bengtsson, W. Yi, “Timed Automata: Semantics, Algorithms and Tools”, Lectures on Concurrency and Petri Nets, LNCS, 3098, no. 5, Springer, 2004, 87–124 | DOI

[14] W. M. Zuberek, “Timed Petri Nets Definitions, Properties and Applications”, Microelectronics Reliability, 31:4 (1991), 627–644 | DOI

[15] A. J. Boudjadar, J. H. Kim, K. G. Larsen et al., “Model Checking Process Algebra of Communicating Resources for Real-time Systems”, ECRTS (Madrid, Spain, July 8–11, 2014), Proceedings of the 26th Euromicro Conference on Real-Time Systems, 51–60 | DOI

[16] D. Lime, O. H. Roux, C. Seidner et al., “Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches”, TACAS (York, UK, March 22–29, 2009), Tools and Algorithms for the Construction and Analysis of Systems, LNCS, 5505, Springer, 54–57 | DOI

[17] T. Henzinger, “The Theory of Hybrid Automata”, Verification of Digital and Hybrid Systems, NATO ASI Series, 170, Springer, 2000, 265–292 | DOI

[18] N. P Buslenko, Complex Systems Modeling, Nauka, Moscow, 1978, 400 pp.

[19] E. Andre, “Observer Patterns for Real-Time Systems”, ICECCS (Singapore, July 17-19, 2013), Proceedings of the 18th IEEE International Conference on Engineering of Complex Computer Systems, 125–134 | DOI

[20] Avionics Application Software Standard Interface. ARINC Specification 653., Aeronautical Radio, Annapolis, 1997