Quantitative Static Analysis Over Semirings: Analysing Cache Behaviour for Java Card

We present a semantics-based technique for modeling and analysing resource usage behaviour of programs written in a simple object oriented language like Java Card byte code. The approach is based on the quantitative abstract interpretation framework of Di Pierro and Wiklicky where programs are represented as linear operators. We consider in particular linear operators over semi-rings (such as max-plus) that have proven useful for analysing cost properties of discrete event systems. We illustrate our technique through a cache behaviour analysis for Java Card.