The Quantitative Analysis of Approximate Correctness for Real-Time Systems

doi:10.23940/ijpe.17.06.p10.886896

Abstract

Abstract: 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.

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.
References: 24

Yanfang Ma, Liang Chen, and Haiyu Pan. The Quantitative Analysis of Approximate Correctness for Real-Time Systems [J]. Int J Performability Eng, 2017, 13(6): 886-896.

Add to citation manager EndNote|Reference Manager|ProCite|BibTeX|RefWorks

References 0

	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
	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.
	C. A. R. Hoare, “Communication Sequential Processes,” Prentice Hall, New York, 1985.
	C. Peter, J. Mesegure, “Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-time System,” Theoretical Computer Science, 451:1-37, 2012.
	G. D. Plotkin, “A Structural Approach to Operational Semantics,” Technical Report DAIMI FN-19, Computer Science Department, Aarhus University,1981.
	J. C. M. Baeten, J. Bergstra, “Real-Time Process Algebra,” Formal Aspects of Computing, 3:142-188, 1991.
	J. Sproston, “Model Checking for Probabilistic Timed Systems,” Lectrue Notes in Compuer Science, 2925:189-229, 2004.
	K. G. Larsen, Y. Wang, “Time-Abstract Bisimulation: Implicit Specifications and Decidability,” Information and Comoputation, 134: 75-101, 1997.
	L Guoqiang, L Li, “Asynchronous Multi-process Timed Automata,” Softwar Quality Control, 2017, DOI: 10.1007/s11219-017-9380-8.
	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.
	M. Bianchia, C. Mereghettib, B. Palano, “Quantum finite automata: Advances on Bertonis ideas,” Theoretical Computer Science, 664: 39-53, 2017.
	M. Hennesy, T. Regan, “A Process Algebra for Timed Systems,” Information and Computation,117: 221-239, 1995.
	M. Krichen, S. Tripakis, “Conformance Testing for Real-Time Systems,” Formal Methods in System Design, 2009, 34: 238-304.
	M. S. Ying, “Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrency Programs,” Springer-Verlag, 2001.
	M. S. Ying, “Bisimulation Indexes and Their Applications,” Theoretical Computer Science, 275(1-2): 1-68, 2002.
	R. Engelking, “General Topology,” Polish Science, 1977.
	M. Hennesy, T. Regan, “A Process Algebra for Timed Systems,” Information and Computation, 117: 221-239, 1995.
	R. Milner. “Communication and Concurrency,” Prentice Hall, New York,1989.
	V. Gupta, T. A. Henzinger, R. Jagadeesan, “Robust Timed Automata,” Lectrue Notes in Compuer Science, 1201: 331-345, 1997.
	X. Hu, R. S. Sambandam, “Multi-Valued Performance Metrics for Real-Time Embedded Systems,” Design Automation for Embedded Systems, 5: 5-28, 2000
	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.
	Y. Wang, “Real-Time Behaviour of Asynchronous Agents,” in Proceeding of CONCUR’90, Lecture Notes in Computer Science, 458: 502-520, 1990.
	Y. Wang, “CCS + Time = an Interleaving Model for Real Time Systems,” Lecture Note in Computer Science, 1991, 510: 217-228.
	Y. Wang, “A Calculus of Real Time Systems,” Ph.D thesis, Chalmers University,1991.