Model Checking Abstract State Machines

Model Checking Abstract State Machines
Kirsten Winter (著)

Model Checking Abstract State Machines

Product Description
The benefits of formal methods have been discussed many times in the literature. Production costs can be decreased greatly if errors can be detected in an early phase of design. Accidents, involving majordamage and even loss of lives, can be avoided if systems are working correctly. Nevertheless, the use of formal methods is limited in practice since the trade-off between productivity and reliability isstill too large. This work aims at improving the applicability of the formal approach.To be of practical relevance in the future formal system development must provide support for modelling and analysis. Currently, however, there is a discrepancy between tools that are easy to use due toautomation and languages that nicely support the modelling task. It is necessary to bridge this gap. This work contributes with a solution for a particular formal language and a particular kind of tool support for verification. The title ''Model Checking Abstract State Machines summarises the results."

About the Author
Kirsten Winter studied Computer Science at the University ofErlangen/Nuernberg and the University of Freiburg (at theInstitute of Computer Science and Social Research, IIG). She receivedthe Ph.D. degree in computer science from the Technical UniversityBerlin, in 2001. She currently holds a position as a researchfellow at the University of Queensland, Australia. Her researchinterests includes the verification of software and hardware systems,mainly model checking, as well as formal modelling notations.