首页>
外国专利>
USING FINITE STATE AUTOMATA TO VERIFY SYSTEMS SUBJECT TO DELAY CONSTRAINTS
USING FINITE STATE AUTOMATA TO VERIFY SYSTEMS SUBJECT TO DELAY CONSTRAINTS
展开▼
机译:使用有限状态自动机验证受延迟约束的系统
展开▼
页面导航
摘要
著录项
相似文献
摘要
Apparatus for developing and verifying systems. The disclosed apparatus employs a computationally-tractable technique for verifying whether a system made up of a set of processes, each of which has at least one delay constraint associated with it, satisfies a given temporal property. The technique deals with the verification as a language inclusion problem, i.e., it represents both the set of processes and the temporal property as automata and determines whether there is a restriction of the set of processes such that the language of the automaton representing the restricted set of processes is included in the language of the automaton representing the temporal property. The technique is computationally tractable because it deals with the problem iteratively: it tests whether a current restriction of the set of processes is included, and if not, it employs a counter-example for the inclusion to either determine that the delay constraints render satisfaction of the given temporal property or to derive a new restriction of the set of processes. Further included in the disclosure are techniques for checking the timing consistency of the counter-example with respect to a delay constraint and techniques for finding the optimal delay constraint.
展开▼