000190680 001__ 190680
000190680 005__ 20190316235747.0
000190680 037__ $$aREP_WORK
000190680 245__ $$aUniform Analysis for Communicating Timed Systems (Extended Technical Report)
000190680 269__ $$a2013
000190680 260__ $$c2013
000190680 300__ $$a21
000190680 336__ $$aReports
000190680 520__ $$aLanguages based on the theory of timed automata are a well established approach for modelling and analysing real-time systems, with many applications both in an industrial and academic context. Model checking for timed automata has been studied extensively during the last two decades; however, even now industrial-grade model checkers are available only for few timed automata dialects (in particular UPPAAL timed automata), exhibit limited scalability for systems with large discrete state space, and cannot handle parametrised systems, or systems with unboundedly many processes. Leveraging recent advances of general-purpose fixed-point engines, we present a flexible method for translating networks of timed automata to Horn constraints, which can then be solved via of-the-shelf solvers. The resulting analysis method is fully symbolic and applicable to systems with large or infinite discrete state space, can be extended to include various language features, for instance UPPAAL-style communication/broadcast channels and BIP-style interactions, and can analyse systems with infinite parallelism. Experiments with timed automata models demonstrate the feasibility of the method.
000190680 6531_ $$ak-indexed Invariant
000190680 6531_ $$aTimed Automata
000190680 6531_ $$aHorn Clause
000190680 6531_ $$aInvariant Schema
000190680 6531_ $$aCounter-Example Guided Abstraction Refinement
000190680 6531_ $$aBIP
000190680 700__ $$0242189$$g185231$$aHojjat, Hossein
000190680 700__ $$aRuemmer, Philipp
000190680 700__ $$aSubotic, Pavle
000190680 700__ $$aYi, Wang
000190680 8564_ $$uhttps://infoscience.epfl.ch/record/190680/files/main.pdf$$zPreprint$$s457939$$yPreprint
000190680 909C0 $$xU12523$$0252413$$pRISD
000190680 909CO $$ooai:infoscience.tind.io:190680$$qGLOBAL_SET$$pIC$$preport
000190680 917Z8 $$x185231
000190680 937__ $$aEPFL-REPORT-190680
000190680 973__ $$aEPFL
000190680 980__ $$aREPORT