2003 DNS Frisco

Finite Model Generation for Distributed Java Programs: 

Finite Model Generation for Distributed Java Programs Eric MADELAINE Rabea BOULIFA INRIA Sophia-Antipolis, France

Context: 

Context Analysis and verification software platform for distributed Java applications. Pervasive and mobile computing, e-commerce, grid computing Long term goal: full language, usable by non-specialists Automatic tools = static analysis, model-checkers, equiv / preorder checkers. Graphical / Logical Specifications Code analysis Finite model Automatic tools, diagnostics, etc.

Slide3: 

Software verification: ESC-Java, CADP, Slam, Blast, Feaver, Bandera, JPF So, what’s special with distributed applications ? Asynchronous communication error-prone, state explosion Structured: composition of distributed components hierarchical construction / reduction / analysis of models bisimulation semantics Well-defined, architecture-independent semantics with the ProActive Library. Inherit methods and tools from existing software: Static analysis from Soot. Slicing / abstraction from Bandera. Standard or prototype checkers (action based)

Related Work: 

Related Work ESC-JAVA : Java code, pre-post conditions, invariants on methods data, “debug oriented”. CADP : Lotos code, simulation, test generation, model-checking, equivalence checking. SLAM : C code, pointer analysis and boolean abstraction, device driver verification, Bebop and Moped checkers. BLAST : C code, abstraction refinement, temporal safety properties. FEAVER : C code (large telecom software), properties as logic, automata, or diagram, model extraction, Spin. BANDERA - JPF: Sequential and multi-threaded Java code, slicing and abstraction, Spin or others.

Outline: 

Outline Distributed Java Applications, the ProActive Library Models: Parameterised Networks of LTSs Model Construction Verification Platform Conclusion

Distributed Java Applications: the ProActive Library: 

Distributed Java Applications: the ProActive Library Features : distributed, mobile, heterogeneous. Transparent distribution no shared data between distributed objects. Message semantics (method calls + request queue) => delivery guarantied by the middleware (MOP). Requests and responses : transparent future objects with “wait by necessity”.

ProActive: Communication Scheme: 

ProActive: Communication Scheme Local object Remote object

Model: Parameterised Networks of synchronised LTSs: 

Model: Parameterised Networks of synchronised LTSs Actions = Requests/Responses (method name + finite abstraction of arguments) Finite Extended LTSs (integer variables) Synchronisation Networks [Arnold 80] Global action < *, …, L1, …, L2, …, * Concrete syntax : FC2 intermediate language extended for encoding integer parameters [st>0] ?stamp-> st--

Model Construction (1): Nets: 

Model Construction (1): Nets Finitely many active objects class / creation points User provided approximation of arguments (abstract interpretation to finite or integer domains) => Boxes and Links computed by static analysis (dataflow, reference and alias analysis) Q1 + A1 Q2 + A2 Req (M, args) Rep (v) Q3 + A3 P(k)

Model Construction (2): Activities: 

Model Construction (2): Activities 1 LTS per activity Construction by SOS rules, based on the Method Call Graph of the active object. Termination guarantied (for a finite data abstraction) => Rules and proofs in the full paper: http://www-sop.inria.fr/oasis/Vercors

Model Construction: Queues: 

Model Construction: Queues Arbitrary unbounded structures, usually regular, depending on the inspection primitives used in the code. We use finite approximations. In many interesting cases it can be proved that a bounded size is enough (global property of the system). Factorisation / optimisation of the model by code analysis.

Parameterised Verification Methods: 

Parameterised Verification Methods Model Construction Parameterised Specification : Parameterised networks / Parameterised logics Source Code Finite Instantiation

Conclusion: 

Conclusion Behaviour models of ProActive distributed applications encode asynchronous communication between distributed objects. With usual data/structure abstraction, we build finite, hierarchical, models suitable for automatic verification. Parameterised models can be finitely instantiated (adapted to each property), or directly fed into specialised tools. They are more compact and more flexible. Case Study: Chilean electronic tax system Other ProActive features : group communication, security policy specification. Behaviour specification for distributed components (in ObjectWeb / Fractal) Directions