Stopwatch Automata-Based Model for Efficient Schedulability Analysis of Modular Computer Systems

  • Alevtina GloninaEmail author
  • Anatoly Bahmurov
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10421)


In this paper we propose a stopwatch automata-based model of a modular computer system operation. This model provides an ability to perform schedulability analysis for a wide class of modular computer systems. It is formally proven that the model satisfies a set of correctness requirements. It is also proven that all the traces, generated by the model interpretation, are equivalent for schedulability analysis purposes. The traces equivalence allows to use any trace for analysis and therefore the proposed approach is much more efficient than Model Checking, especially for parallel systems with many simultaneous events. The software implementation of the proposed approach is also presented in the paper.


Stopwatch automata Integrated modular avionics Simulation Schedulability analysis 


  1. 1.
    Avionics application software standard interface: ARINC specification 653. Aeronautical Radio, Annapolis (1997)Google Scholar
  2. 2.
    AUTOSAR. Enabling Innovation.
  3. 3.
    Obermaisser, R., et al.: DECOS: an integrated time-triggered architecture. Elektrotech. Inftech. 123(3), 83–95 (2006). doi: 10.1007/s00502-006-0323 CrossRefGoogle Scholar
  4. 4.
    Marinescu, S., et al.: Timing analysis of mixed-criticality hard real-time applications implemented on distributed partitioned architectures. In: Proceedings of 2012 17th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2012), Krakow, Poland, pp. 1–4 (2012). doi: 10.1109/ETFA.2012.6489720
  5. 5.
    Macariu, G., Cretu, V.: Timed automata model for component-based real-time systems. In: Proceedings of 2010 17th IEEE International Conference and Workshops on Engineering of Computer Based Systems, Oxford, UK, pp. 121–130 (2010). doi: 10.1109/ECBS.2010.20
  6. 6.
    Craveiro, J.P., Silveira, R.O., Rufino, J.: hsSim: an extensible interoperable object-oriented n-level hierarchical scheduling simulator. In: Proceedings of the 3rd International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems (WATERS 2012), Pisa, Italy, pp. 9–14 (2012)Google Scholar
  7. 7.
    Khoroshilov, A., et al.: AADL-based toolset for IMA system design and integration. SAE Int. J. Aerosp. 5(2), 294–299 (2012). doi: 10.4271/2012-01-2146 CrossRefGoogle Scholar
  8. 8.
    Balashov, V.V., Balakhanov, V.A., Kostenko, V.A.: Scheduling of computational tasks in switched network-based IMA systems. In: Proceedings of International Conference on Engineering and Applied Sciences Optimization, Athens, Greece, pp. 1001–1014 (2014)Google Scholar
  9. 9.
    Cassez, F., Larsen, K.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 138–152. Springer, Heidelberg (2000). doi: 10.1007/3-540-44618-4_12 CrossRefGoogle Scholar
  10. 10.
    Tretyakov, A.: Automation of scheduling for periodic real-time systems (in Russian). Proc. Inst. Syst. Program. 22, 375–400 (2012). doi: 10.1134/S0361768813050046 CrossRefGoogle Scholar
  11. 11.
    Bengtsson, J., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-27755-2_3 CrossRefGoogle Scholar
  12. 12.
    Andre, E.: Observer patterns for real-time systems. In: Proceedings of 2013 18th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), Singapore, pp. 125–134 (2013). doi: 10.1109/ICECCS.2013.26

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Lomonosov Moscow State UniversityMoscowRussia

Personalised recommendations