دانلود مقاله ISI انگلیسی شماره 17238
ترجمه فارسی عنوان مقاله

مبدل CAP جاوا کارت در PVS

عنوان انگلیسی
A Java Card CAP converter in PVS
کد مقاله سال انتشار تعداد صفحات مقاله انگلیسی
17238 2004 17 صفحه PDF
منبع

Publisher : Elsevier - Science Direct (الزویر - ساینس دایرکت)

Journal : Electronic Notes in Theoretical Computer Science, Volume 82, Issue 2, April 2004, Pages 426–442

ترجمه کلمات کلیدی
کارت جاوا - مبدل -
کلمات کلیدی انگلیسی
Java Card,converter,
پیش نمایش مقاله
پیش نمایش مقاله  مبدل CAP جاوا کارت در PVS

چکیده انگلیسی

The Java Card language is a trimmed down dialect of Java aimed at programming smart cards. Java Card specifies its own class file format (the Java Card Converted APplet (CAP) format) that is optimised with respect to the limited space resources of smart cards. This paper deals with the certified development of algorithms necessary for the conversion of ordinary Java class files into the CAP format. More precisely, these algorithms are concerned with constructing and compressing method tables and constant pools. The main contribution of this paper is to specify and prove the correctness of these algorithms using the theorem prover PVS.

مقدمه انگلیسی

The Java Card language [7] is a trimmed down dialect of Java aimed at programming smart cards. As with Java, Java Card is compiled into bytecode, which is then verified and executed on a virtual machine [4], installed on a chip on the card itself. However, the memory and processor limitations of smart cards necessitate a further stage, in which the bytecode is optimised from the standard class file format of Java, to the CAP file format [8]. The core of this optimisation is a tokenization in which names (strings) are replaced with tokens (integer values). Replacing strings with integers reduces the size of the code and enables a faster lookupof virtual methods using the standard object-oriented technique of vtables. Additional optimisations are obtained by a componentisation that merges class files from the same package into one CAP file. This means that data which is common to several class files can be