随着数字系统设计日益复杂化，对于系统设计和实现正确性的要求越来越高。如何在整个系统设计代码空间中定位到满足给定性质的模块，从而验证设计模块满足设计者的要求;如何在发现错误时，通过自动化方式定位到问题代码片段，这些都是在保证系统设计正确性的过程中涉及到的问题，且存在于数字系统设计流程中的各个阶段。执行验证技术的算法对所采用规范语言的类型十分敏感，由于时序逻辑具有表达能力强、直观、兼容性好等特点，能够很好地表达程序的安全性、活性和事件优先性等性质。因此，时序逻辑己广泛应用于程序的规约、验证和形式化开发，以及程序自动综合和模块化规范合成等并发程序设计的各个方面。　　 本文就在整个系统设计空间中定位满足给定规范的模块的问题，提出了一种关于时序逻辑的静态性质验证技术。通过研究规范的可实现性问题，将规范和系统转化成相应的状态机，并通过搜索能够精化规范的必胜策略的Mealy机，来实现在整个设计中搜索满足规范的模型。与模型检测不同的是，本问题严格区分输入、输出命题变量，并要求规范是可实现的;无需指明待验证的系统模块，特别是在错误定位时，本身就不知道要验证的是哪个系统模块，而不像模型检测需给定系统模型。　　 本文侧重在时序逻辑框架下研究规范的可实现性问题:由LTL公式描述的规范可得到等价的Büchi自动机，在对应自动机基础上可将该问题规约为运行环境和系统的二人博弈，定义了在博弈中系统的必胜策略。采用Mealy型有限状态机描述必胜策略，并由此延伸出Mealy状态机之间的精化关系，给出了精化检验算法以及系统设计空间的必胜策略检测的搜索框架。通过检测算法可在整个设计中搜索满足给定规范的模型。该技术可应用于定位电路设计中满足给定功能规范的信号。若结合不应该出现的规范性质，也可用于定位系统设计中的问题代码片段，实现错误定位。