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

fYear

2014

fDate

27-29 June 2014

Firstpage

105

Lastpage

110

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering and Service Science (ICSESS), 2014 5th IEEE International Conference on

Conference_Location

Beijing

ISSN

2327-0586

Print_ISBN

978-1-4799-3278-8

Type

conf

DOI

10.1109/ICSESS.2014.6933523

Filename

6933523