2003 DNS Frisco

50 %
50 %
Information about 2003 DNS Frisco
Entertainment

Published on October 29, 2007

Author: Crystal

Source: authorstream.com

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

Add a comment

Related presentations

Related pages

Montblanc Watches, Writing Instruments, Leather & Jewellery

Visit the Official Montblanc website to discover the timeless beauty of Montblanc watches, writing instruments, jewellery, leather goods, fragrance and ...
Read more

Ericsson - A world of communication - Ericsson

Ericsson is shaping the future of mobile broadband Internet communications through its continuous technology leadership, helping to create the most ...
Read more

Google

De missie van Google is alle informatie ter wereld te organiseren en universeel toegankelijk en bruikbaar te maken.
Read more

getpics.online - Berlin Hub

© 2016 by bring the pixel. Remember to change this. Back to Top
Read more

Official Apple Support

Apple support is here to help. Learn more about popular topics and find resources that will help you with all of your Apple products.
Read more

Results 8/9/03 - Village Creek Motocross Park

August 9th, 2003. Race Results. Finish: Number: Brand: Name: City,State: Moto 1: Moto 2; 250cc Novice; 1: ... Frisco, TX: 6: DNS 9: 8r: HON: Mike Shirley ...
Read more

Scan to E-mail White Paper - Ricoh USA

7 SCAN TO E-MAIL IN WINDOWS SERVER 2000 OR 2003 ... Scan to E-mail White Paper ... To avoid potential DNS problems,
Read more

Land Rover Deutschland | Above and Beyond | Modellübersicht

Die einzigartige Land Rover DNS bildet auch heute noch den Kern all unseres Schaffens. Entdecken Sie die Ausstattung unserer vielseitigen Premium-SUVs.
Read more

Wells Fargo - Personal & Business Banking - Student, Auto ...

Wells Fargo is a provider of banking, mortgage, investing, credit card, insurance, and consumer and commercial financial services.
Read more

Google

Advertising Programmes Business Solutions +Google About Google Google.com © 2016 - Privacy - Terms. Search; Images; Maps; Play; YouTube; News; Gmail ...
Read more