Abstract | ||
---|---|---|
In smart card embedded programs, some operations must not be suddenly interrupted, because if they are, the card is left in an inconsistent state. Since the card can be removed at any time from the terminal, which interrupts any running program, some instructions must be executed at each reset in order to verify if a tearing occurred and to restore a consistent state if necessary. In this case, the card is said to ensure the anti-tearing property. This paper presents a method to formally prove that a C program verifies the anti-tearing property for a given "tearing-sensitive operation. The back-ground methodology, presented in [1], [2], enables to prove global properties from source code. It is here illustrated by the proof of anti-tearing properties, which requires an extension of the method in order to specify and verify functions behaviour in the case of a sudden interruption of their execution. |
Year | DOI | Venue |
---|---|---|
2006 | 10.1109/ISoLA.2006.14 | ISoLA |
Keywords | Field | DocType |
embedded program,functions behaviour,c code,source code,global property,c program,smart card,back-ground methodology,consistent state,anti-tearing property,inconsistent state,embedded systems,smart cards | BasicCard,Programming language,Card reader,Source code,Computer science,Smart card,Java Card,Answer to reset,OpenPGP card,Smart card application protocol data unit | Conference |
Citations | PageRank | References |
2 | 0.40 | 6 |
Authors | ||
1 |
Name | Order | Citations | PageRank |
---|---|---|---|
June Andronick | 1 | 903 | 42.66 |