Practical Automaton proofs in PVS
In case you object to the disclosure of your thesis, you can contact firstname.lastname@example.org
[S.l. : s.n.]
Number of pages
RU Radboud Universiteit Nijmegen, 6 maart 2008
Promotor : Vaandrager, F.W. Co-promotor : Hooman, J.J.M.
Display more detailsDisplay less details
Informatics for Technical Applications
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.
Upload full text
Use your RU credentials (u/z-number and password) tolog in with SURFconextto upload a file for processing by the repository team.