Behavior Analysis of Real-Time Systems Using PLA Method

  • Dalius Makackas
  • Regina Miseviciene
  • Henrikas Pranevicius
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 403)


The paper deals with a behavior analysis task of real-time system specified by the PLA method. An algorithm for creating a reachable state graph is used while solving for the task. The algorithm evaluates intervals of time when the defined system events occur. An approach based on the algorithm for the reachable state graph generation is presented within this paper. The suggested approach is illustrated by an example.


real -time system analysis trajectory modeling reachable state graph 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aceto, L., Bouyer, P., Burgueno, A., Larsen, K.G.: The power of reachability testing for timed automata. Theoretical Computer Science 300, 411–475 (2003)Google Scholar
  2. 2.
    Bonhomme, P.: Scheduling and control of real-time systems based on a token player approach. Discrete Event Dynamic Systems 23, 197–209 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Buslenko, N.P., Kalashnikov, V.V., Kovalenko, I.N.: Lectures on the Theory of Complex Systems. Sov. Radio, Moscow (1973) (in Russian)Google Scholar
  4. 4.
    Dang, Z., Ibarra, O.H., Kemmerer, R.A.: Generalized discrete timed automata: decidable approximations for safety verification. Theoretical Computer Science 296, 59–74 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    David, R., Alla, H.: On hybrid Petri nets. Discrete Event Dynamic Systems 11, 9–40 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Ding, Z., Jiang, C., Zhou, M.: Design, Analysis and Verification of Real-Time Systems Based on Time Petri Net Refinement. ACM Transactions on Embedded Computing Systems (TECS) 12 (2013)Google Scholar
  7. 7.
    Ghomri, L., Alla, H.: Modeling and analysis using hybrid Petri nets. Nonlinear Analysis: Hybrid Systems 1, 141–153 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Gómez, R.: Model-checking timed automata with deadlines with Uppaal. Formal Aspects of Computing 25, 289–318 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11, 157–185 (1997)CrossRefGoogle Scholar
  10. 10.
    Knorreck, D., Apvrille, L., Pacalet, R.: Formal system-level design space exploration. Concurrency and Computation: Practice and Experience 25, 250–264 (2013)CrossRefGoogle Scholar
  11. 11.
    Kopetz, H.: Real-time systems: design principles for distributed embedded applications. Springer Science+ Business Media (2011)Google Scholar
  12. 12.
    Krena, B., Vojnar, T.: Automated formal analysis and verification: an overview. International Journal of General Systems 42, 335–365 (2013)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Laplante, P.A.: Real-Time Systems Design and Analysis. Wiley-IEEE Press (2004)Google Scholar
  14. 14.
    Lorin, H., Deitel, H.M.: Operating Systems. Longman Higher Education (2009)Google Scholar
  15. 15.
    Mekki, A., Ghazel, M., Toguyeni, A.: Validation of a New Functional Design of Automatic Protection Systems at Level Crossings with Model-Checking Techniques. IEEE Transactions Intelligent Transportation Systems 13, 714–723 (2012)CrossRefGoogle Scholar
  16. 16.
    Pranevicius, H.: Complex systems formalization and analysis (in Lithuanian). Technologija, Kaunas (2008)Google Scholar
  17. 17.
    Pranevicius, H., Raudys, S., Rudzionis, A., Ratkevicius, K., Sakalauskaite, J., Makackas, D.: Agent system models. Mokslo aidai, Vilnius (2008)Google Scholar
  18. 18.
    Pranevicius, H., Miseviciene, R.: Verification of piece-linear aggregate specifications. Kaunas, Technologija (2006)Google Scholar
  19. 19.
    Renganathan, K., Bhaskar, V.: Performance evaluation and model checking in systems modeled as Hybrid Petri nets. Applied Mathematical Modelling 36, 3941–3947 (2012)CrossRefGoogle Scholar
  20. 20.
    Saadawi, H., Wainer, G.: Principles of Discrete Event System Specification model verification. Simulation 89, 41–67 (2013)CrossRefGoogle Scholar
  21. 21.
    Yin, Y., Liu, B., Ni, H.: Real-time embedded software testing method based on extended finite state machine. Systems Engineering and Electronics 23, 276–285 (2012)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Dalius Makackas
    • 1
  • Regina Miseviciene
    • 1
  • Henrikas Pranevicius
    • 1
  1. 1.Faculty of InformaticsKaunas University of TechnologyKaunasLithuania

Personalised recommendations