Erik Poll, Joachim van den Berg, Bart Jacobs: Formal specification of the JavaCard API in JML: the APDU class. Comput. Networks 36(4): 407-421 (2001)