Title :
A case study of verifying TFM requirements specification based on SMV
Author :
Xuehang Chi ; Ying Jin ; Jing Zhang
Author_Institution :
Coll. of Comput. Sci. & Technol., JiLin Univ., Changchun, China
Abstract :
With the development of software requirements engineering multiple methods to write requirements specification have been proposed. TFM is a formal specification method proposed by Professor David Parnas and Marius Dragomiroiu, and it is more flexible then previous algebra and axiom methods. SMV is a model checking technique developed by Carnegie Mellon University. This paper proposes a method of verifying TFM requirements specification based on SMV, and makes an application of this method on a small library access control system.
Keywords :
authorisation; formal specification; formal verification; libraries; Carnegie Mellon University; SMV; TFM requirements specification verification; algebra methods; axiom methods; formal specification method; library access control system; model checking technique; software requirements engineering; Access control; Educational institutions; Input variables; Libraries; Loading; Model checking; Software; SMV verification; TFM specification; state machine modeling;
Conference_Titel :
Software Engineering and Service Science (ICSESS), 2014 5th IEEE International Conference on
Conference_Location :
Beijing
Print_ISBN :
978-1-4799-3278-8
DOI :
10.1109/ICSESS.2014.6933523
