Specification of real-time systems using a timed automata modelwith shared variables and verification of partial-deadlock freeness

摘要

We propose a timed automata model with shared variables (TASV). ATASV is a set of extended timed automata (ETAs) with shared booleanvariables. For this model, we propose (I) an algorithm which decideswhether a given TASV is partial-deadlock free, and (2) a sufficientcondition that we can efficiently prove a given TASV is partial-deadlockfree. Each ETA in a TASV can access to /modify, shared boolean variablesindependently. By constructing a tuple automaton for all ETAs in a givenTASV we can decide the existence of deadlocks. However, such an approachcauses the state explosion problem. Our algorithm and our proposedsufficient condition reduce the possibility of the state explosion bydividing the ETAs into some sets and proving their partial-deadlockfreeness independently