Title :
The verification technique of real-time systems using probabilities
Author_Institution :
Dept. of Comput. Sci., Shimane Univ., Matue, Japan
Abstract :
Real-time systems are distributed, and require reliability. The formal verification and specification are important for real-time systems. In this paper, in order to obtain reliability, we think the notion of dense-time and probabilities are necessary. We propose the following methods in order to specify and verify performance properties in dense time model. (1) Probabilistic and dense time statecharts and temporal logic (2) An automatic verification method by probabilistic and dense time model checking
Keywords :
formal specification; formal verification; probability; real-time systems; temporal logic; automatic verification method; dense time model; dense time model checking; dense time statecharts; formal specification; formal verification; performance properties; probabilities; real-time systems; reliability; temporal logic; verification technique; Algebra; Automatic logic units; Cities and towns; Computer science; Distributed algorithms; Formal verification; Probabilistic logic; Real time systems; Safety; Timing;
Conference_Titel :
Real-Time Computing Systems and Applications, 1996. Proceedings., Third International Workshop on
Conference_Location :
Seoul
Print_ISBN :
0-8186-7626-4
DOI :
10.1109/RTCSA.1996.554965
