Automated Technology for Verification and Analysis

Name: Automated Technology for Verification and Analysis | 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011, Proceedings

Tevfik Bultan Pao-Ann Hsiung(Herausgeber*in)

Springer (Verlag)

Erschienen am 1. Oktober 2011

XIV, 532 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-24372-1 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Title
Preface
Organization
Table of Contents
Invited Papers
Statistical Model Checking for Cyber-Physical Systems
Introduction
Background
Statistical Model Checking
The Monte Carlo Method
Importance Sampling
Basics
The Cross-Entropy Method
Experiments
Conclusions
References
Max and Sum Semantics for Alternating Weighted Automata
Introduction
Alternating Weighted Automata
The Max Semantics
The Duality between the Min and the Max Semantics
Expressive Power
Arithmetics
The Sum Semantics
Exponential Weights
Expressive Power
sum-UWA and Polynomials
Discussion
References
Making Software Verification Tools Really Work
Introduction
Community Support for Tool Development
Allocating Resources to Tool Development
The Need for Robust Tools
Program Semantics: Minimum Requirements
What Should All Software Verification Tools Handle, a minima?
The Challenges of Semantic Features in Real-World Languages
The Lack of Guidance in the Process of Writing Tools
Proposals for Supporting the Development of Software Verification Tools
Publication Incentives
Benefits from Building Tools
Standards for Tool Interfaces
Benchmarks to Drive Quality, Comparability, and Competition
Summary
References
Synthesizing, Verifying, and Debugging SoC with FSM-Based Specification of On-Chip Communication Protocols
Introduction
FSM-Based Specification of On-Chip Communication Protocols
Automatic Generation of On-Chip Communication Protocol Converters
Post-Silicon Verification and Debugging of SoC with FSM-Based Specifications of On-Chip Communication Protocols
Concluding Remarks
References
Automated Analysis of Industrial Embedded Software
Introduction
Unified Storage Platform for OneNAND Flash Memory
Overview of the Unified Storage Platform
Logical-to-Physical Sector Translation
Analysis Results and Discussions
Concolic Testing Technique
Samsung Linux Platform (SLP) for Smartphones
File Manager
Security Library
Conclusion and Future Work
References
Regular Papers
Nondeterministic Update of CTL Models by Preserving Satisfaction through Protections
Introduction
Technical Preliminaries
CTL Update Algorithms
Nondeterministic Pseudo-Code
Modification of Models
A Direct Update Algorithm for -XCTL
An Algorithm for Updating Protected Models
Model Update for -CTL and Addition of States
Soundness and Completeness of XUpdprot
Synthesizing a Model of the Mutual Exclusion Problem
Related Work and Conclusions
References
Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols
Introduction
Processes
Type System
Basic Ideas
Types
Typing
Type Inference
Implementation and Experiments
Extensions
Related Work
References
Formalization of Finite-State Discrete-Time Markov Chains in HOL
Introduction
Related Work
Probability Theory and Random Variables in HOL
Formal Modeling of Discrete-Time Markov Chains
Verification of Discrete-Time Markov Chain Properties
Joint Probability of a Markov Chain
Chapman-Kolmogorov Equation
Absolute Probabilities
Steady State Probabilities
Generalized Stationary Distribution
Application: Binary Communication Channel
Conclusions
References
An Alternative Definition for Timed Automata Composition
Introduction
Related Work
A New Composition of Timed Automata
Differences with Existing Approaches
Benefits of the Proposal
Transformation to Basic Uppaal
Transition System Extensions
Labelled Transition Systems
Composable Labelled Transition Systems
Product of Composable Labelled Transition Systems
CLTS with Location Invariants
Timed Transition Systems Extensions
ETTS Timed Traces
Networks of Timed Automata
Timed Automata
Semantics of Timed Automata
Networks of Timed Automata
Semantics of a NTA
Composition and Refinement
Conclusion
References
Model Checking EGF on Basic Parallel Processes
Introduction
Preliminaries
Model Checking the Logic EGF
Fixed Formula
Conclusion
References
Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited
Introduction
Preliminaries
Mean-Payoff Parity Games
Mean-Penalty Parity Games
Conclusion
References
Algorithms for Synthesizing Priorities in Component-Based Systems
Introduction
Component-Based Modeling and Priority Synthesis
Behavioral-Interaction-Priority Framework
Priority Synthesis for Safety and Deadlock Freedom
A Framework of Priority Synthesis Based on Fault-Localization and Fault-Repair
System Encoding
Step A. Finding Fix Candidates Using Fault-Localization
Step B. Priority Synthesis via Conflict Resolution - From Stateful to Stateless
Optimization
Handling Complexities
Data Abstraction
Alphabet Abstraction
Assume-Guarantee Based Priority Synthesis
Evaluation
Related Work
Conclusion
References
Trust Metrics for the SPKI/SDSI Authorisation Framework
Introduction
Formal Definitions
Complexity of Computing the Trust Metrics
Approximation of the Trust Metrics
Spookey and Experimental Results
Future Work
References
Antichain-Based QBF Solving
Introduction
Preliminaries
Notations and QBF Problem
QBF Problem as a Game
Structure in the And-Or Graph and Antichains
Algorithms
Maximal and Minimal Valuations
Antichain-Based Algorithm
Certificates
Optimizations
Guiding the Search to Promising Valuations
Improving the Information about Losing and Winning Nodes
Experimental Results
Conclusion and Perspectives
References
A Hierarchical Approach for the Synthesis of Stabilizing Controllers for Hybrid Systems
Introduction
Controller Synthesis for Stabilization Games
Stabilization Games
Algorithm for Stabilization Games
Nonlinear Systems and Discretizations
Nonlinear Systems with Inputs
Discretizations
Hierarchical Approach to Controller Synthesis
Abstractions Preserving Controllability
Hierarchical Abstractions in ODE Systems
Experiments
Conclusions and Future Work
References
Formal Analysis of Online Algorithms
Introduction
Preliminaries
Weighted Automata
Online Algorithms
An Automata-Theoretic Approach to Reasoning about Online Algorithms
Adding Assumptions on the Environment
Reasoning about Online Algorithms with Look-Ahead
Symbolic Model-Checking Algorithm
References
Modal Transition Systems: Composition and LTL Model Checking
Introduction
Preliminaries
LTL Model Checking
Parallel Composition
Common Implementation Problem and Conjunction
Conclusion and Future Work
References
Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata
Introduction
Preliminaries
Downward Inclusion Checking
Basic Algorithm of Downward Inclusion Checking
Optimized Algorithm of Downward Inclusion Checking
Experimental Results
Semi-symbolic Representation of Tree Automata
Binary Decision Diagrams
Encoding the Transition Function of a TA Using Shared MTBDDs
Downward Simulation on Semi-symbolically Encoded TA
Downward Inclusion Checking on Semi-symbolically Encoded TA
Experimental Results
Conclusion
References
Assembling Sessions
Introduction
Motivational Example
Session Systems
Preliminaries
Session Schemes
Sessions
Agents
Scheduling
Semantics of Session Systems
Conclusion
References
Parametric Modal Transition Systems
Introduction
Parametric Modal Transition Systems
Motivation
Definition of Parametric Modal Transition System
Modal Refinement
Complexity of Modal Refinement Checking
Parameter-Free Systems
Systems with Parameters
Conclusion and Future Work
References
Policy Iteration within Logico-Numerical Abstract Domains
Introduction
Abstract Interpretation and Abstract Domains
Abstract Equation Solving and Policy Iteration
Integrating Policies in Numerical Abstract Domains
Policy for Logico-Numerical Abstract Domain
Experiments
Conclusion
References
Small Strategies for Safety Games
Introduction
Safety Games and Strategies
Learning Small Strategies
A Teacher for Strategy Automata
An Improved Learning Algorithm
Main Result
Experiments
Conclusion
References
Multi-core Nested Depth-First Search
Introduction
Background (LTL Model Checking)
Related Work
Multi-core Ndfs
A Basic Multi-core Swarmed Ndfs
Multi-core Ndfs with Global Coloring
Correctness Proof
Extensions
Experiments
Models with Accepting Cycles
Models without Accepting Cycles
Conclusions
References
Self-Loop Aggregation Product - A New Hybrid Approach to On-the-Fly LTL Model Checking
Introduction
Preliminaries
Boolean Formulas
TGBA
Kripke Structure
Self-Loop Aggregation Product (SLAP)
Definition
Proof of Correctness
Mixing SLAP and Fully Symbolic Approaches
Experimentations
Implementation
Benchmark
Conclusion and Perspectives
References
A Lightweight Approach for Loop Summarization
Introduction
Inferring Summary Constraints
Cycle Exit Information
Inter Variable Relations
Quantified Array Formulas
Function Infer
Cycle Elimination
Divergence (Cycle) Detection
Cycle Replacement
Extended CEGAR
Integrating Loop Summarization into CEGAR
Experimental Evaluation
Related Work
Conclusion
References
A Succinct Canonical Register Automaton Model
Introduction
Data Languages and Register Automata
Symbolic Representation of Data Languages
Nerode Congruence and Canonical Form
Comparison between Different Automata Models
Conclusions and Future Work
References
Parallel Nested Depth-First Searches for LTL Model Checking
Introduction
Background
The LTL Model Checking Problem
Algorithms Based on Nested Depth-First Search
Parallel Algorithms for LTL Model Checking
mc-ndfs, a Multi-core Algorithm for LTL Model Checking
Difficulty of Parallelising ndfs
Principle of the Algorithm
Details of the Algorithm
Proof of the Algorithm
Complexity of the Algorithm
Using Tarjan's Algorithm in Nested Searches
Experimental Results
Conclusion and Perspectives
References
Evaluating LTL Satisfiability Solvers
Introduction
Preliminaries
Solvers
Benchmarks
Methodology
Results
Potential of a Portfolio Solver
Conclusion
References
Tool Papers
McAiT - A Timing Analyzer for Multicore Real-Time Software
Introduction
Main Features and Implementation of McAiT
References
MIO Workbench: A Tool for Compositional Design with Modal Input/Output Interfaces
Context
Tool Architecture
Experiments and Future Work
References
Short Papers
The Buck Stops Here: Order, Chance, and Coordination in Distributed Control
Introduction
Knowledge Based Control in a Nutshell
Reducing Process Hanging and Passing Responsibility
Refinig Knowledge
References
Symbolic Verification and Test Generation for a Network of Communicating FSMs
Introduction
Preliminaries
Decision Diagrams
Previous Work
System Framework and Symbolic Encoding
Symbolic NCFSM Verification
Symbolic NCFSM Test Derivation
Experimental Results
Conclusion
References
Hierarchical Counterexamples for Discrete-Time Markov Chains
Introduction
Preliminaries
SCC-Based Model Checking
Counterexample Generation
The Basic Hierarchical Algorithm
Search Algorithms
Experimental Results
References
Efficient Loop Navigation for Symbolic Execution
Introduction
Overview
The Algorithm
Experimental Results
Related Work
References
An Efficient Algorithm for Learning Event-Recording Automata
Introduction
Preliminaries
Timed Languages and Event-Recording Automata
The L* Algorithm
An Efficient Algorithm for Learning ERA
The TL* Algorithm
Analysis of the TL* Algorithm
Conclusion and Future Work
References
Discretizing Affine Hybrid Automata with Uncertainty
Introduction
Affine Hybrid Automata with Uncertainty
From Affine Hybrid Automata to Affine Programs
Conclusion
References
What's Decidable about Weighted Automata?
Introduction
Preliminaries
Weighted Automata with Integer Weights
Weighted Automata with Positive Weights
Universality Is PSPACE-Complete
Containment Is Undecidable
References
Widening with Thresholds for Programs with Complex Control Graphs
Introduction and Related Work
The Widening/Narrowing Approach in Practice
Inferring Thresholds by Propagating Disjunctions
Experiments and Conclusion
References
Linear Hybrid System Falsification through Local Search
Introduction
Problem Formulation
Descent in the Robustness Ellipsoid
Experiments
Conclusions
References
Learning-Based Compositional Verification for Synchronous Probabilistic Systems
Introduction
Preliminaries
Assume-Guarantee for Synchronous Probabilistic Systems
Deciding Language Inclusion for PFAs
L*-Style Learning for PFAs
Learning Assumptions for Compositional Verification
Implementation and Results
References
An Algorithmic Framework for Synthesis of Concurrent Programs
Introduction
Algorithmic Framework
Correctness of Synthesis
Extensions and Experiments
Concluding Remarks
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken