DocumentCode :
3260938
Title :
Specification of real-time systems using a timed automata model with shared variables and verification of partial-deadlock freeness
Author :
Okano, Kozo ; Hattori, Satoshi ; Yamamoto, Akira ; Higashino, Teruo ; Taniguchi, Kenichi
Author_Institution :
Graduate Sch. of Eng., Osaka Univ., Japan
fYear :
1999
fDate :
1999
Firstpage :
576
Lastpage :
581
Abstract :
We propose a timed automata model with shared variables (TASV). A TASV is a set of extended timed automata (ETAs) with shared boolean variables. For this model, we propose (I) an algorithm which decides whether a given TASV is partial-deadlock free, and (2) a sufficient condition that we can efficiently prove a given TASV is partial-deadlock free. Each ETA in a TASV can access to /modify, shared boolean variables independently. By constructing a tuple automaton for all ETAs in a given TASV we can decide the existence of deadlocks. However, such an approach causes the state explosion problem. Our algorithm and our proposed sufficient condition reduce the possibility of the state explosion by dividing the ETAs into some sets and proving their partial-deadlock freeness independently
Keywords :
automata theory; concurrency control; formal specification; real-time systems; TASV; extended timed automata; partial-deadlock free; partial-deadlock freeness; real-time systems; shared boolean variables; shared variables; timed automata model; Automata; Explosions; Formal specifications; Real time systems; Sufficient conditions; System recovery; Time of arrival estimation; Timing;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Parallel Processing, 1999. Proceedings. 1999 International Workshops on
Conference_Location :
Aizu-Wakamatsu
ISSN :
1530-2016
Print_ISBN :
0-7695-0353-5
Type :
conf
DOI :
10.1109/ICPPW.1999.800118
Filename :
800118
Link To Document :
بازگشت