Skip to main content
SpringerLink
Log in

Behavior Analysis of Real-Time Systems Using PLA Method

  • Conference paper
Information and Software Technologies (ICIST 2013)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 403))

Included in the following conference series:

  • 1722 Accesses

Abstract

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.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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. Bonhomme, P.: Scheduling and control of real-time systems based on a token player approach. Discrete Event Dynamic Systems 23, 197–209 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  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. Dang, Z., Ibarra, O.H., Kemmerer, R.A.: Generalized discrete timed automata: decidable approximations for safety verification. Theoretical Computer Science 296, 59–74 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  5. David, R., Alla, H.: On hybrid Petri nets. Discrete Event Dynamic Systems 11, 9–40 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  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. Ghomri, L., Alla, H.: Modeling and analysis using hybrid Petri nets. Nonlinear Analysis: Hybrid Systems 1, 141–153 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  8. Gómez, R.: Model-checking timed automata with deadlines with Uppaal. Formal Aspects of Computing 25, 289–318 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  10. Knorreck, D., Apvrille, L., Pacalet, R.: Formal system-level design space exploration. Concurrency and Computation: Practice and Experience 25, 250–264 (2013)

    Article  Google Scholar 

  11. Kopetz, H.: Real-time systems: design principles for distributed embedded applications. Springer Science+ Business Media (2011)

    Google Scholar 

  12. Krena, B., Vojnar, T.: Automated formal analysis and verification: an overview. International Journal of General Systems 42, 335–365 (2013)

    Article  MathSciNet  Google Scholar 

  13. Laplante, P.A.: Real-Time Systems Design and Analysis. Wiley-IEEE Press (2004)

    Google Scholar 

  14. Lorin, H., Deitel, H.M.: Operating Systems. Longman Higher Education (2009)

    Google Scholar 

  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)

    Article  Google Scholar 

  16. Pranevicius, H.: Complex systems formalization and analysis (in Lithuanian). Technologija, Kaunas (2008)

    Google Scholar 

  17. Pranevicius, H., Raudys, S., Rudzionis, A., Ratkevicius, K., Sakalauskaite, J., Makackas, D.: Agent system models. Mokslo aidai, Vilnius (2008)

    Google Scholar 

  18. Pranevicius, H., Miseviciene, R.: Verification of piece-linear aggregate specifications. Kaunas, Technologija (2006)

    Google Scholar 

  19. Renganathan, K., Bhaskar, V.: Performance evaluation and model checking in systems modeled as Hybrid Petri nets. Applied Mathematical Modelling 36, 3941–3947 (2012)

    Article  Google Scholar 

  20. Saadawi, H., Wainer, G.: Principles of Discrete Event System Specification model verification. Simulation 89, 41–67 (2013)

    Article  Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. Faculty of Informatics, Kaunas University of Technology, Studentu 56-443, Kaunas, Lithuania

    Dalius Makackas, Regina Miseviciene & Henrikas Pranevicius

Authors
  1. Dalius Makackas
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Regina Miseviciene
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Henrikas Pranevicius
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Kaunas University of Technology, Studentu g. 50-313a, 51368, Kaunas, Lithuania

    Tomas Skersys

  2. Centre of Information Systems Design Technologies, Kaunas University of Technology, Studentu st. 50-313a, 51368, Kaunas, Lithuania

    Rimantas Butleris

  3. Kaunas University of Technology, Studentu g. 50-309a, 51368, Kaunas, Lithuania

    Rita Butkiene

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Makackas, D., Miseviciene, R., Pranevicius, H. (2013). Behavior Analysis of Real-Time Systems Using PLA Method. In: Skersys, T., Butleris, R., Butkiene, R. (eds) Information and Software Technologies. ICIST 2013. Communications in Computer and Information Science, vol 403. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41947-8_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-41947-8_33

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-41946-1

  • Online ISBN: 978-3-642-41947-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation