A Formal Specification of Mondex Using SAM

Author

Zeng, Reng ; Liu, Jianling ; He, Xudong

Author_Institution

Sch. of Comput. & Inf. Sci., Florida Int. Univ., Miami, FL, USA

fYear

2008

fDate

18-19 Dec. 2008

Firstpage

97

Lastpage

102

Abstract

This paper presents a formal specification of Mondex, an electronic purse, using SAM. Mondex is the first pilot project for the 6th Grand Challenge to develop an integrated, automated toolset that developers can use to establish the correctness of software. Several research groups around the world have applied different formal methods in specifying and analyzing the Mondex smart card since 2006. Our specification is unique, which uses a software architecture model integrating high level Petri nets and temporal logic; thus contributes to the world wide effort in tackling one of the grand challenges in computer sciences.

Keywords

Petri nets; formal specification; smart cards; software architecture; temporal logic; Mondex smart card; Petri nets; SAM; formal specification; software architecture; temporal logic; Formal specifications; Helium; Information security; Logic; Petri nets; Smart cards; Software architecture; Software systems; Software tools; Systems engineering and theory; Formal Methods; Grand Challenges; Mondex; Software Architecture; high level Petri nets;

fLanguage

English

Publisher

ieee

Conference_Titel

Service-Oriented System Engineering, 2008. SOSE '08. IEEE International Symposium on

Conference_Location

Jhongli

Print_ISBN

978-0-7695-3499-2

Electronic_ISBN

978-0-7695-3499-2

Type

conf

DOI

10.1109/SOSE.2008.25

Filename

4730470