Mondex Electronic Purse

37

FAC
2010

107views more FAC 2010»

Atomic actions, and their refinements to isolated protocols

13 years 9 months ago

Inspired by the properties of the refinement development of the Mondex Electronic Purse, we view an isolated atomic action as a family of transitions with a common before-state, an...

Richard Banach, Gerhard Schellhorn

claim paper

Read More »

30

click to vote

FAC
2008

88views more FAC 2008»

The certification of the Mondex electronic purse to ITSEC Level E6

14 years 15 days ago

Download www-users.cs.york.ac.uk

Ten years ago the Mondex electronic purse was certified to ITSEC Level E6, the highest level of assuranceforsecuresystems.ThisinvolvedbuildingformalmodelsintheZnotation,linkingthem...

Jim Woodcock, Susan Stepney, David Cooper, John A....

claim paper

Read More »

40

click to vote

FAC
2008

127views more FAC 2008»

Mechanising Mondex with Z/Eves

14 years 15 days ago

Download www.vdmportal.org

We describe our experiences in mechanising the specification, refinement, and proof of the Mondex Electronic Purse using the Z/Eves theorem prover. We took a conservative approach ...

Leo Freitas, Jim Woodcock

claim paper

Read More »

32

click to vote

ENTCS
2008

75views more ENTCS 2008»

On the Refinement of Atomic Actions

14 years 16 days ago

Download www.cs.man.ac.uk

Inspired by the properties of the refinement development of the Mondex Electronic Purse, we view an atomic action as a family of transitions with a common before-state, and differ...

Richard Banach, Gerhard Schellhorn

claim paper

Read More »

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers