Automata-Based Programming Technology Extension for Generation of JML Annotated Java Card Code
Andrey Klebanov, Alexander Mikhaylov · Proceedings of the Spring/Summer young researchers' colloquium on software engineering · 2008
This paper gives an overview of the ongoing research project which concerns generation of dependable Java Card code.According to the automata-based programming technology, 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 description is the possibility of generation of formal application specification in Java Modeling Language.Conformance of the code against its specification could be checked by different static checking and verification tools.