Handling contract violations in Java Card using explict exception channels

Java Card is a version of Java developed to run on devices with severe storage and processing restrictions. The applets that run on these devices are frequently intended for use in critical, highly distributed, mobile conditions. This requires runtime verification approach based on Design by Contract to improve the safety of Java Card applications. However handling contract violation in Java Card applications is challenging due to their communication structure and platform restrictions. Additionally the Java Card exception handling mechanism requires that developers understand the source of an exception, the place where it is handled, and everything in between. As system development evolves, exceptional control flows become less well-understood, with negative consequences for the program maintainability and robustness. In this paper, we claim that such problem can be addressed by implementing an innovative exception handling model which provides abstractions to explicitly describe global views of exceptional control flows.