DocumentCode :
2626336
Title :
Modelling and verification of a network player system with DCValid
Author :
Jianzhong, Wang ; Qiwen, Xu ; Huadong, Ma
Author_Institution :
Int. Inst. for Software Technol., United Nations Univ., Macau, China
fYear :
2000
fDate :
2000
Firstpage :
44
Lastpage :
49
Abstract :
In this paper we study the formal modelling and verification of a network player system using Duration Calculus, a real time interval temporal logic. The system is modelled by the conjunction of a number of Duration Calculus formulae each capturing a basic property of the system. That the system satisfies the requirement is expressed by the entailment of the requirement formula from the system formula. We use an automated tool DCValid for verification. DCValid is a model checking tool and it cannot verify our system in the general form, and therefore a special instance is derived from the general model and subsequently checked using DCValid
Keywords :
formal specification; formal verification; multimedia systems; temporal logic; DCValid; Duration Calculus; automated tool; formal modelling; formal verification; model checking tool; network player system; real time interval temporal logic; Calculus; Computer science; Educational institutions; Games; Internet telephony; Logic; Multimedia systems; Real time systems; Video on demand; Videoconference;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Quality Software, 2000. Proceedings. First Asia-Pacific Conference on
Conference_Location :
Hong Kong
Print_ISBN :
0-7695-0825-1
Type :
conf
DOI :
10.1109/APAQ.2000.883777
Filename :
883777
Link To Document :
بازگشت