Geodesic
Automata-based approach for correct Java Card-program
Modelirovanie i analiz informacionnyh sistem, Tome 15 (2008) no. 3, pp. 47-55.

Voir la notice de l'article provenant de la source Math-Net.Ru

The paper gives an overview of the research project which considers the generation of the dependable *Java Card* code. According to the automata-based programming technology, the code is generated from a high-level application behavior description which is based on finite state machines. An extra benefit from the use of such an approach is the possibility of the formal application specification generation. The conformance of the source or byte code against its specification could be checked by different static checking and verification tools. 
@article{MAIS_2008_15_3_a4,
     author = {A. A. Klebanov and A. A. Shalyto},
     title = {Automata-based approach for correct {Java} {Card-program}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {47--55},
     publisher = {mathdoc},
     volume = {15},
     number = {3},
     year = {2008},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2008_15_3_a4/}
}
TY  - JOUR
AU  - A. A. Klebanov
AU  - A. A. Shalyto
TI  - Automata-based approach for correct Java Card-program
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2008
SP  - 47
EP  - 55
VL  - 15
IS  - 3
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2008_15_3_a4/
LA  - ru
ID  - MAIS_2008_15_3_a4
ER  - 
%0 Journal Article
%A A. A. Klebanov
%A A. A. Shalyto
%T Automata-based approach for correct Java Card-program
%J Modelirovanie i analiz informacionnyh sistem
%D 2008
%P 47-55
%V 15
%N 3
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2008_15_3_a4/
%G ru
%F MAIS_2008_15_3_a4
A. A. Klebanov; A. A. Shalyto. Automata-based approach for correct Java Card-program. Modelirovanie i analiz informacionnyh sistem, Tome 15 (2008) no. 3, pp. 47-55. http://geodesic.mathdoc.fr/item/MAIS_2008_15_3_a4/

[1] Zh. Chen, Tekhnologiya Java Card dlya smart-kart. Arkhitektura i rukovodstvo programmista, Tekhnosfera, M., 2008

[2] NASA LaRC Formal Methods Program: What is Formal Methods?, http://shemesh.larc.nasa.gov/fm/fm-what.html

[3] A. A. Shalyto, “Algoritmizatsiya i programmirovanie dlya sistem logicheskogo upravleniya i «reaktivnykh» sistem”, Avtomatika i telemekhanika, 2001, no. 1, 3–39 | Zbl

[4] E. Poll, J. van den Berg, B. Jacobs, “Specification of the JavaCard API in JML”, Proc. Fourth Smart Card Research and Advanced Application Conference, 135–154

[5] A. Coglio, “An Approach to the Generation of High-Assurance Java Card Applets”, Proc. 2nd NSA Conf. on High Confidence Software and Systems (HCSS'02), 2002, 69–77

[6] E. Hubbers, M. Oostdijk, E. Poll, “From finite state machines to provably correct Java Card applets”, Proc. 18th IFIP Inform. Security Conf., 2003, 465–479

[7] V. S. Gurov, M. A. Mazin, A. A. Shalyto, “UniMod - instrumentalnoe sredstvo dlya avtomatnogo programmirovaniya”, Nauchno-tekhnicheskii vestnik. Fundamentalnye i prikladnye issledovaniya informatsionnykh sistem i tekhnologii, 30, SPbGU ITMO, 2006, 32–44 http://is.ifmo.ru/works/_instrsr.pdf

[8] E. Hubbers, M. Oostdijk, “Generating JML specifications from UML state diagrams”, Proc. Forum on specification and Design Languages (FDL'03), 2003, 263–273

[9] Razrabotka tekhnologii verifikatsii upravlyayuschikh programm so slozhnym povedeniem, postroennykh na osnove avtomatnogo podkhoda, Promezhutochnyi otchet po II etapu «Teoreticheskie issledovaniya postavlennykh pered NIR zadach», SPbGU ITMO, 2007 http://is.ifmo.ru/verification/_2007_02_report-verification.pdf

[10] S. E. Velder, A. A. Shalyto, “Vvedenie v verifikatsiyu avtomatnykh programm na osnove metoda Model checking”, Nauchno-tekhnicheskii vestnik. Fundamentalnye i prikladnye issledovaniya informatsionnykh sistem i tekhnologii, 42, SPbGU ITMO, 2007, 33–48 http://vestnik.ifmo.ru/ntv/ntv_42.1.5.pdf

[11] V. A. Nepomnyaschii, O. M. Ryakin, Prikladnye metody verifikatsii programm, Radio i svyazyu, M., 1988

[12] E. V. Kuzmin, V. A. Sokolov, “O verifikatsii \flqqavtomatnykh\frqq programm”, Aktualnye problemy matematiki i informatiki, Sbornik statei k 20-letiyu fakulteta IVT YarGU im. P. G. Demidova, Yaroslavl, 2006, 27–32 http://is.ifmo.ru/verification/_verautpr.pdf

[13] G. A. Korneev, V. G. Parfenov, A. A. Shalyto, “Verifikatsiya avtomatnykh programm”, Tezisy dokladov Mezhdunarodnoi nauchnoi konferentsii, posvyaschennoi pamyati professora A. M. Bogomolova \flqq Kompyuternye nauki i tekhnologii\frqq, SGU, Saratov, 2007, 66–69 http://is.ifmo.ru/verification/_KNIT-2007.pdf

[14] E. M. Clarke, J. M. Wing, “Formal methods: State of the Art and Future Directions”, ACM Computing Surveys, 4 (1996), 626–643 | DOI

[15] B. Meier, Ob'ektno-orientirovannoe konstruirovanie programmnykh sistem, Russkaya redaktsiya, M., 2005

[16] G. T. Leavens, Y. Cheon, Design by Contract with JML, http://www.jmlspecs.org/jmldbc.pdf

[17] G. T. Leavens, A. L. Baker, C. Ruby, Preliminary design of JML: A behavioral interface specification language for Java, Tech. Rep. 98-06u, Apr., Iowa State Univ., Dept. of Comput. Sci., 2003

[18] L. Burdy, “An overview of JML tools and applications”, Int. J. on Software Tools for Technology Transfer (STTT), 7:3 (2005), 212–232 | DOI

[19] D. Harel, A. Pnueli, “On the Development of Reactive Systems”, Logic and Models of Concurrent Systems, NATO Advanced Study Institute on Logic and Models for Verification and Specification of Concurrent Systems, 1985, 477–498 | MR | Zbl

[20] A. A. Shalyto, “Avtomatnoe proektirovanie programm. Algoritmizatsiya i programmirovanie zadach logicheskogo upravleniya”, Izvestiya RAN. Teoriya i sistemy upravleniya, 2000, no. 6, 63–81 http://is.ifmo.ru/download/app-aplu.pdf

[21] D. G. Shopyrin, A. A. Shalyto, “Sinkhronnoe programmirovanie”, Informatsionno-upravlyayuschie sistemy, 2004, no. 3, 35–42 http://is.ifmo.ru/works/sync_prog_024.pdf

[22] A. A. Shalyto, “Paradigma avtomatnogo programmirovaniya /A. A. Shalyto”, Materialy mezhdunarodnoi nauchno-tekhnicheskoi konfrentsii «Mnogoprotsessornye vychisleniya i upravlyayuschie sistemy», Mezhdunarodnaya nauchno-tekhnicheskaya multikonferentsiya «Problemy informatsionnykh tekhnologii i mekhatroniki», 1, NIIMVS, Taganrog, 2007, 191–194 http://is.ifmo.ru/works/_2007_09_27_shalyto.pdf

[23] A. A. Shalyto, N. I. Tukkel, “Switch-tekhnologiya – avtomatnyi podkhod k sozdaniyu programmnogo obespecheniya «reaktivnykh» sistem”, Programmirovanie, 2001, no. 5, 45–62 http://is.ifmo.ru/works/switch/1/ | Zbl