A unified approach to real-time specification, verification, and analysis: finite models and beyond

实时规范、验证和分析的统一方法：有限模型及其他

• 批准号: 262103-2008
• 负责人: Bruda, Stefan
• 金额: $ 1.09万
• 依托单位: Bishop's University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2011
• 资助国家: 加拿大
• 起止时间: 2011-01-01 至 2012-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=480156
• 关键词: unified; approach; real; time; specification

Software verification is more or less an empirical process in today's industrial practice: Tests are applied to software in the hope that these tests cover most of the functionality and thus discover most (but certainly not all) of the bugs. Another approach is conformance testing (our interest): A piece of software is checked against a formal model (the specification) in a fully automated (and efficient) manner. In a first variant (model checking), the specification consists in a logical formula, which is checked against the implementation; in a second variant (model-based testing) the specification takes an algebraic form and is then compared with the implementation either directly or via systematic test suites.

软件验证在今天的工业实践中或多或少是一个经验性的过程：对软件进行测试，希望这些测试覆盖大部分功能，从而发现大部分（但肯定不是全部）错误。另一种方法是一致性测试（我们感兴趣的）：以完全自动化（和有效）的方式对照正式模型（规范）检查软件。在第一种变体（模型检查）中，规范包含在一个逻辑公式中，并针对实现进行检查;在第二种变体（基于模型的测试）中，规范采用代数形式，然后直接或通过系统测试套件与实现进行比较。