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
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;
Conference_Titel :
Parallel Processing, 1999. Proceedings. 1999 International Workshops on
Conference_Location :
Aizu-Wakamatsu
Print_ISBN :
0-7695-0353-5
DOI :
10.1109/ICPPW.1999.800118