Practical Automaton proofs in PVS

Abstract

This thesis is about an approach to modeling, validating and verifying com- puter-based systems. The kinds of systems we examine happen to be em- bedded systems, for the most part, but our approach is generally applicable to computer-based systems. Since veri?cation is essential to the production of safe and reliable systems, we feel the entire process that precedes the actual construction of such a system is in need of formal support; various studies in this thesis show how a systematic approach to modeling and val- idation can be applied to part of the software development lifecycle: the requirements and speci?cation phases. We focus on the practical side of modeling and validation, showing how to approach problems of ambiguity and incompleteness in the informal requirements. We illustrate some of the considerations used in arriving at the approach used in this thesis. The case studies and considerations show how this approach can be effective in ?nd- ing errors in models - errors which, when corrected, lead to better models and higher quality computer-based systems.