Specifying and Checking Java using CSP
Michael Möller · 2002
Abstract. Currently several approaches are done in applying formal techniques to the Java programming language. A new trend is to take dynamic behaviour into account when designing such techniques. To bring formal techniques to practical applications one often has to reduce the goal coming down from full verification to runtime checking. jassda [5,4] is a framework for performing such runtime checks at the bytecode level of Java. The Trace-Checker module of jassda allows one to test the dynamic behaviour of multiple Java virtual machines by monitoring whether the trace of all relevant events is a member of the trace semantics of a given CSP process or not. In this paper we present the CSP dialect that is used to specify a set of allowed traces for Java programs. The underlying semantics allow partial specification of distributed Java programs and to recombine them while preserving properties. 1