期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2010
卷号：39
页码：91-99
DOI：10.4204/EPTCS.39.7
出版社：Open Publishing Association
摘要：We present here Imitator II, a new version of Imitator, a tool implementing the "inverse method" for parametric timed automata: given a reference valuation of the parameters, it synthesizes a constraint such that, for any valuation satisfying this constraint, the system behaves the same as under the reference valuation in terms of traces, i.e., alternating sequences of locations and actions. Imitator II also implements the "behavioral cartography algorithm", allowing us to solve the following good parameters problem: find a set of valuations within a given bounded parametric domain for which the system behaves well. We present new features and optimizations of the tool, and give results of applications to various examples of asynchronous circuits and communication protocols.
