Username   Password       Forgot your password?  Forgot your username? 

The Quantitative Analysis of Approximate Correctness for Real-Time Systems

Volume 13, Number 6, October 2017 - Paper 10  - pp. 886-896
DOI: 10.23940/ijpe.17.06.p10.886896

Yanfang Maa,*, Liang Chenb, Haiyu Panc

aSchool of Computer and Science, Huaibei Normal University, Huaibei,China, 235000
bSchool of Mathematical Science, Huaibei Normal University, Huaibei,China, 235000
cTaizhou University, Taizhou,China, 235000

(Submitted on July 25, 2017; Revised on August 30, 2017; Accepted on September 15, 2017)

(This paper was presented at the Third International Symposium on System and Software Reliability.)


In order to formalize the correctness of real-time systems, strong timed bisimulation in TCCS has been proposed to characterize the relation between implementation and specification. The usual action and time delay must be the same in strong timed bisimulation. However, in some real situations, many real-timed systems can not satisfy the exact match. In this paper, in order to characterize the approximate usual action and time delay, the strong timed bisimulation in TCCS is generalized to numerical version. Firstly, the definition of global timed bisimulation index of a binary relation is established to describe the relation between implementation and specification. Secondly, in order to quantify the approximate degree between implementation and specification, the global timed lambda-bisimulation is defined. Finally, the congruence of the global timed lambda-bisimulation is proven to guarantee the modular development and hierarchic design methods which are used in the real software development.


References: 24

    1. C. Baier, J. Katoen, D. Latella, “Metric Semantics for True Concurrent Real Time,” International Colloquium on Automata, Languages, and Programming, 254(1–2): 568-579, 1998
    2. C. Baier, N. Bertrand, T. Brihaye, T. Brihaye, “Probabilistic and topological semantics for timed automata,” In Proceeding of the 27th International Conference on Foundations of Software Technology and Theoretical Computer Science, 4855 :179-191, 2007.
    3. C. A. R. Hoare, “Communication Sequential Processes,” Prentice Hall, New York, 1985.
    4. C. Peter, J. Mesegure, “Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-time System,” Theoretical Computer Science, 451:1-37, 2012.
    5. G. D. Plotkin, “A Structural Approach to Operational Semantics,” Technical Report DAIMI FN-19, Computer Science Department, Aarhus University,1981.
    6. J. C. M. Baeten, J. Bergstra, “Real-Time Process Algebra,” Formal Aspects of Computing, 3:142-188, 1991.
    7. J. Sproston, “Model Checking for Probabilistic Timed Systems,” Lectrue Notes in Compuer Science, 2925:189-229, 2004.
    8. K. G. Larsen, Y. Wang, “Time-Abstract Bisimulation: Implicit Specifications and Decidability,” Information and Comoputation, 134: 75-101, 1997.
    9. L Guoqiang, L Li,  “Asynchronous Multi-process Timed Automata,” Softwar Quality Control, 2017, DOI: 10.1007/s11219-017-9380-8.
    10. L Guoqiang , W Yueqing, Y Shoyi, “Updatable Timed Automata with One Updatable Clock,” Science in China Series F Information Sciences, DOI: 10.1007/s11432-016-9027-y, 2017.
    11. M. Bianchia, C. Mereghettib, B. Palano, “Quantum finite automata: Advances on Bertonis ideas,” Theoretical Computer Science, 664: 39-53, 2017.
    12. M. Hennesy, T. Regan, “A Process Algebra for Timed Systems,” Information and Computation,117: 221-239, 1995.
    13. M. Krichen, S. Tripakis, “Conformance Testing for Real-Time Systems,” Formal Methods in System Design, 2009, 34: 238-304.
    14. M. S. Ying, “Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrency Programs,” Springer-Verlag, 2001.
    15. M. S. Ying, “Bisimulation Indexes and Their Applications,” Theoretical Computer Science, 275(1-2): 1-68, 2002.
    16. R. Engelking, “General Topology,” Polish Science, 1977.
    17. M. Hennesy, T. Regan, “A Process Algebra for Timed Systems,” Information and Computation, 117: 221-239, 1995.
    18. R. Milner. “Communication and Concurrency,” Prentice Hall, New York,1989.
    19. V. Gupta, T. A. Henzinger, R. Jagadeesan, “Robust Timed Automata,” Lectrue Notes in Compuer Science, 1201: 331-345, 1997.
    20. X. Hu, R. S. Sambandam, “Multi-Valued Performance Metrics for Real-Time Embedded Systems,” Design Automation for Embedded Systems, 5: 5-28, 2000
    21. Y. F. Ma, M. Zhang, Y. X. Chen, L.Chen, “Two-thirds Simulation Indexes and Modal Logic Characterization,” Frontiers of Computer Science in China, 5(4) , 454-471, 2011.
    22. Y. Wang, “Real-Time Behaviour of Asynchronous Agents,” in Proceeding of CONCUR’90, Lecture Notes in Computer Science, 458: 502-520, 1990.
    23. Y. Wang, “CCS + Time = an Interleaving Model for Real Time Systems,” Lecture Note in Computer Science, 1991, 510: 217-228.
    24. Y. Wang, “A Calculus of Real Time Systems,” Ph.D thesis, Chalmers University,1991.


      Click here to download the paper.

      Please note : You will need Adobe Acrobat viewer to view the full articles.Get Free Adobe Reader

      This site uses encryption for transmitting your passwords.