CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

A Program Logic for Handling Java Card's Transaction Mechanism

Bernhard Beckert ; Wojciech Mostowski (Institutionen för datavetenskap)
Lecture Notes in Computer Science. Joint European Conference on Theory and Practice of Software (ETAPS 2003), Warsaw, 5-13 April 2003 (0302-9743). Vol. 2621 (2003), p. 246-260.
[Konferensbidrag, refereegranskat]

In this paper we extend a program logic for verifying Java Card applications by introducing a "throughout" operator that allows us to prove "strong" invariants. Strong invariants can be used to ensure "rip out" properties of Java Card programs (properties that are to be maintained in case of unexpected termination of the program). Along with introducing the "throughout" operator, we show how to handle the Java Card transaction mechanism (and, thus, conditional assignments) in our logic. We present sequent calculus rules for the extended logic.

Nyckelord: Java, Java Card, object-oriented programming, atomic transactions, formal specification, formal verification, Dynamic Logic



Denna post skapades 2006-08-25. Senast ändrad 2013-02-20.
CPL Pubid: 1841

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för datavetenskap (2002-2004)

Ämnesområden

Information Technology

Chalmers infrastruktur

Relaterade publikationer

Denna publikation ingår i:


Towards Development of Safe and Secure Java Card Applets