Formal Methods for System Development
Master thesis
Permanent lenke
http://hdl.handle.net/11250/259936Utgivelsesdato
2009Metadata
Vis full innførselSamlinger
Sammendrag
Two main types of formal methods have been investigated, formal specification and formal verification. Focus for formal verification has been on the concept of un-timed model checking. Some dominating formal specification languages, VDM and Z, and some prominent model checkers, FDR, Spin, and LTSA, have been learnt and presented. A tutorial for the formal verification tool Spin is created. The tutorial is example driven and describes the description language Promela and the verification methods available in Spin. Care has been taken to illustrate reasoning about the results from Spin. Topics discussed include the applicability and need for formal methods, the possible need for understanding the underlying theory, and considerations made in regards to creating the tutorial.