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 e 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. Key words: Static analysis, resource usage, cache behaviour, linear operators, semirings

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Pascal Sotin, David Cachera, Thomas P. Jensen
• Keywords: ENTCS 2006, Linear Operators, Particular Linear Operators, Resource Usage Behaviour