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

点击翻译按钮获取中文摘要

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.