NASA Formal Methods
Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011, Proceedings
Published on 6. April 2011
XIV, 534 pages
978-3-642-20398-5 (ISBN)
Description
This book constitutes the refereed proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011, held in Pasadena, CA, USA, in April 2011.
The 26 revised full papers presented together with 12 tool papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 141 submissions. The topics covered by NFM 2011 included but were not limited to: theorem proving, logic model checking, automated testing and simulation, model-based engineering, real-time and stochastic systems, SAT and SMT solvers, symbolic execution, abstraction and abstraction refinement, compositional verification techniques; static and dynamic analysis techniques, fault protection, cyber security, specification formalisms, requirements analysis, and applications of formal techniques.
The 26 revised full papers presented together with 12 tool papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 141 submissions. The topics covered by NFM 2011 included but were not limited to: theorem proving, logic model checking, automated testing and simulation, model-based engineering, real-time and stochastic systems, SAT and SMT solvers, symbolic execution, abstraction and abstraction refinement, compositional verification techniques; static and dynamic analysis techniques, fault protection, cyber security, specification formalisms, requirements analysis, and applications of formal techniques.
More details
Other editions
Additional editions
Mihaela Bobaru | Klaus Havelund | Gerard Holzmann
NASA Formal Methods
Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011, Proceedings
Book
04/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- I. Invited Talks
- From Retrospective Verification to Forward-Looking Development
- Specifications for Free
- Introduction
- Specification Mining
- Static Analysis
- Dynamic Invariants
- Exploring Behavior
- Pre- and Postconditions
- Some Challenges
- Domain-Specific Vocabularies
- Exploring Behavior
- Expressive Specifications
- Ranking Specifications
- Integration with Symbolic Approaches
- Scalability and Efficiency
- Related Work
- Conclusion and Consequences
- References
- II. Invited Tutorials
- The Theory and Practice of SALT
- Introduction
- Feature Overview
- Propositional Layer
- Temporal Layer
- Timed Layer
- Macros and Parameterised Expressions
- Further Examples
- Semantics
- Comparison with Existing Approaches
- Overview
- A Comparison of Features
- Further Related Work
- Realisation and Results
- Experimental Results
- Conclusions
- References
- VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java
- Introduction
- Symbolic Execution
- Symbolic Execution States
- Algorithm: Preliminary Definitions
- The Algorithm
- Soundness Proof Sketch
- Permission Accounting
- Fractional Permissions
- Precise Predicates
- Dummy Fractions for Leakable Resources
- Counting Permissions
- Lemma Function Termination and Dynamic Binding
- Ongoing Efforts
- JavaCard Programs
- Integrating Shape Analysis
- Linux Device Drivers
- References
- Verifying Functional Correctness of C Programs with VCC
- References
- III. Regular Papers
- Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic Execution
- Introduction
- Example
- Bakar Kiasan Symbolic Execution Engine
- Checking Spark Contracts in Kiasan
- Bakar Kiasan Methodology and Tools
- Evaluation
- Related Work
- Conclusion and Future Work
- References
- Approximate Quantifier Elimination for Propositional Boolean Formulae
- Introduction
- Quantifier Elimination and Abstract Interpretation
- Quantifier Elimination by Resolution and Striking Out Literals
- Contributions to Approximate Quantifier Elimination
- Existential Quantification in Five Steps
- Under-Approximation Using Implicants
- Over-Approximation Using Implicants
- Approximation Using Prime Implicants
- Solution-Space Reduction Using Instantiation
- Solution-Space Reduction Using Multiple Instantiations
- Correctness of the Transformation
- Transforming Clauses
- Transforming Cubes
- Equivalence
- Experimental Results
- Related Work
- Conclusions
- References
- Towards Flight Control Verification Using Automated Theorem Proving
- Introduction
- Related Work
- MetiTarski : An Automated Theorem Prover
- MetiTarski Input Syntax
- Axioms
- Proposed Methodology
- Case Study : Model 24 Learjet SBJ
- Conclusion and Future Directions
- References
- Generalized Rabin(1) Synthesis with Applications to Robust System Synthesis
- Introduction
- Related Work
- Preliminaries
- Generalized Rabin(1) Synthesis
- Extending Generalized Rabin(1) Synthesis
- Application to Synthesize Robust Systems
- Bounded-Transition-Phase Generalized Rabin(1) Synthesis
- Conclusion
- References
- Integrating an Automated Theorem Prover into Agda
- Introduction
- Agda
- Integration of Automated Theorem Proving
- Proof Cycle Example
- The Reflection Layer
- Proof Reconstruction
- Examples
- Conclusions and Future Work
- References
- Efficient Predicate Abstraction of Program Summaries
- Introduction
- Background
- Program Summary
- Predicate Abstraction of Program Fragments
- Single Static Assignment
- Generating Predicate Abstraction Queries
- Solving Predicate Abstraction Queries
- Experimental Results
- Conclusion
- References
- Synthesis for PCTL in Parametric Markov Decision Processes
- Introduction
- Preliminaries
- Non-parametric Models
- Probabilistic CTL
- Parametric Models
- Hyper-rectangles
- Synthesis for PCTL
- Reward Formula R-3mum( )
- Probabilistic Formula P-3mup()
- Termination and Correctness
- Experiments
- Conclusion
- References
- Formalizing Probabilistic Safety Claims
- Introduction
- Systems
- Modeling Uncertainty in System Variables
- Modeling Hazardous Conditions
- Modeling All Possible Hazardous Conditions
- Probabilistic Safety Claims
- Dependence of System Variables on Hazardous Conditions
- A Proved Safety Claim for Conflict Detection
- GPS and ADS-B Hazardous Conditions
- Probabilistic Kernels in Conflict Detection
- The Safety Claim for Conflict Detection
- Conclusion and Future Work
- References
- The OpenTheory Standard Theory Library
- Introduction
- The OpenTheory Proof Archive
- Articles of Proof
- Theory Packages
- Identifying Core Theories
- Extracting Standard Articles
- Granularity
- Standardization
- Partial Functions
- The Standard Theory Library
- Construction
- Axioms
- Theorems
- Related Work
- Summary
- Future Work
- References
- Instantiation-Based Invariant Discovery
- Introduction
- A General Scheme for Invariant Discovery
- Partial Order Templates
- Binary Domains
- Experimental Evaluation
- Conclusion and Future Work
- References
- Stuttering Mostly Speeds Up Solving Parity Games
- Introduction
- Preliminaries
- Parity Games
- Strong Bisimilarity and Stuttering Equivalence
- Experiments
- Test Sets
- Results
- Discussion
- Conclusions
- References
- Counterexample-Based Error Localization of Behavior Models
- Introduction
- Motivating Example
- Background
- Error Localization Procedure
- Outline
- Constructing WTS Models
- Finding Witnesses
- Identifying Errors
- Implementation and Case Studies
- Discussions and Related Work
- Conclusions
- References
- Call Invariants
- Introduction
- Motivation
- Program without Procedure Calls
- Program with Procedure Calls
- Call Invariants
- Source and Assertion Language
- Call Invariant and Program Instrumentation
- Evaluation
- Dynamic Allocation
- Linked Lists
- Arrays
- Discussion
- Related Work
- Conclusion
- References
- Symmetry for the Analysis of Dynamic Systems
- Introduction
- Graph Transformation System Modelling
- Symmetry in Dynamic GTS Models
- GTS Bisimulation
- Generating a Bisimilar Quotient
- Vertex Bisimulation
- Property Preservation
- Conclusion
- References
- Implementing Cryptographic Primitives in the Symbolic Model
- Introduction
- Applied Pi-calculus
- Secure Implementation of Primitives
- Security of the Implementation of Randomized Symmetric Encryption
- Related Work
- Conclusions
- References
- Model Checking Using SMT and Theory of Lists
- Introduction
- Background
- Approach
- Applicability to Software Model Checking
- The Idea
- Formal Definitions
- Example
- Optimizing Transformations from CFG to PG
- Translation of PG to SMT
- Execution of Live Sequence Charts
- Example
- Motivation
- Solution
- Evaluation and Results
- Related Work
- Conclusion
- References
- Automated Test Case Generation with SMT-Solving and Abstract Interpretation
- Introduction
- SMT Solver
- Modeling Formalism
- Abstract Interpretation
- Conclusion and Evaluation Results
- References
- Generating Data Race Witnesses by an SMT-Based Analysis
- Introduction
- Multithreaded Trace
- Execution Traces
- Partial Order and Linearizations
- Symbolic Encoding of the Write-Read Consistency
- Encoding the Partial Order
- Encoding Write-Read Consistency
- Encoding the Data Race
- Symbolic Encoding of the Synchronization Consistency
- Synchronization Interpretation
- The Recursive-Lock-Free Encoding
- Encoding with Recursive Locks
- Correctness and Complexity
- Static Optimizations
- Experiments
- Conclusion
- References
- Applying Atomicity and Model Decomposition to a Space Craft System in Event-B
- Introduction
- Background
- Event-B and Refinement
- Atomicity Decomposition
- Model Decomposition
- Event-B Model of the Probe System
- An Overview of System Requirements and Development Process
- Abstract Specification
- First Level of Refinement: Introducing Validation Steps
- Second Level of Refinement: Distinguish between Different Types of TCs
- Third Level of Refinement: Refining TCs Processing by the Devices
- Decomposing the Probe Model to the Core and Devices Sub-models
- Further Refinements of the Core Sub-model
- Assessment
- Providing Insight for Appropriate Event Decomposition
- Assessing the Influence of Atomicity Decomposition and Model Decomposition over Each Other
- Related Work
- Conclusion
- References
- A Theory of Skiplists with Applications to the Verification of Concurrent Datatypes
- Introduction
- Fine-Grained Concurrent Lock-Coupling Skiplists
- The Theory of Concurrent Skiplists of Height K: TSLK
- Decidability of TSLK
- A Combination-Based Decision Procedure for TSLK
- Conclusion and Future Work
- References
- CORAL: Solving Complex Constraints for Symbolic PathFinder
- Introduction
- Symbolic Execution
- Symbolic PathFinder
- CORAL Heuristic Solvers
- Search Algorithms
- Optimizations
- Sample Constraints
- Evaluation
- Setup
- Comparison with Other Solvers
- Impact of Number of Iterations on Precision and Runtime
- Analysis of the PISCES Library
- Analysis of the Apollo Lunar Autopilot
- Related Work
- Conclusions
- References
- Automated Formal Verification of the TTEthernet Synchronization Quality
- Introduction
- TTEthernet Clock Synchronization Algorithm
- Clock Synchronization Overview
- First Step Convergence: Compression Master (CM)
- Second Step Convergence: Synchronization Master (SM)
- Clock Synchronization Example
- Automated Formal Verification Procedure
- Proof Method Overview
- Formal Model
- Automated Formal Proof
- Fault-Injection Experiments and Results
- Inconsistent Omission Faulty CM
- Arbitrarily Faulty SM
- Inconsistent Omission Faulty SM and CM
- Inconsistent Omission Faulty CM and Arbitrarily Faulty SM
- Summary of Verification Results
- Conclusion
- References
- Extending the GWV Security Policy and Its Modular Application to a Separation Kernel
- Introduction
- Motivating Example: PikeOS
- Micro-Kernel Layer
- Virtualisation Layer (Separation Kernel)
- The Motivation: Putting the Layers Together
- The GWV Model
- Definitions
- The GWV Security Policy
- Clarifying the GWV Security Policy
- Extending the GWV Model with Subjects
- A Modular Usage of the Modified GWV-Policy
- The Micro-Kernel Model
- The Separation Kernel Model
- The Separation Kernel Security Policy
- An Alternative Way to Instantiate the GWV Model with PikeOS
- Summary
- References
- Combining Partial-Order Reduction and Symbolic Model Checking to Verify LTL Properties
- Introduction
- Symbolic LTL Model Checking
- Transitions Systems
- From LTL to Fair-CTL
- Forward Symbolic Model-Checking
- Partial-Order Reduction
- Process Model
- Partial-Order Reduction with BDDs
- LTL Model Checking with Partial-Order Reduction
- Computation of the Reachable States
- Fair-Cycle Detection
- Correctness
- Evaluation
- Related Work
- Conclusion
- References
- Towards Informed Swarm Verification
- Introduction
- Related Work
- Preliminaries
- Directed Lts Search Techniques
- Systems with Independent Processes
- Systems with Synchronising Processes
- Experiments
- Conclusions
- References
- Scaling Up with Event-B: A Case Study
- Introduction
- Event-B Language
- The Platooning Problem
- Platoons
- Research Goal and System Hypotheses
- State of Vehicles
- Scaling Up with Event-B: Mathematics
- 1D Model Adaptation
- 2D Model Adaptation
- Scaling Up with Event-B: Specification Structure
- Decomposition of Events
- Statistics of the Specifications
- Scaling Up with Event-B: Temporal Properties
- Scaling Up with Event-B: Tools
- Edition and Verification
- Animation Plug-In for Validation
- Breaking Animators
- Scaling Up with Event-B: Process
- Conclusion and Future Works
- References
- IV. Tool Papers
- D-Finder 2: Towards Efficient Correctness of Incremental Design
- Context
- D-Finder 2
- Computing Interaction Invariants in an Incremental Manner: the Theory behind D-Finder2
- Implementation Details
- Availability of the Tool and Example of Use
- Experimental Results
- References
- Infer: An Automatic Program Verifier for Memory Safety of C Programs
- Introduction
- Procedure-Local Bugs
- Infer
- Bi-abduction and Compositional Analysis
- Infer's Architecture
- Implementation
- Related Work and Conclusions
- References
- Model Construction and Priority Synthesis forSimple Interaction Systems
- Introduction
- Visualizing Simple Interaction Systems
- Priority Synthesis
- Safety Synthesis by Adding Global Priorities: Examples
- Safety Synthesis by Adding Global Priorities: Algorithmic Issues
- Evaluation and Summary
- References
- OpenJML: JML for Java 7 by Extending OpenJDK
- The Java Modeling Language
- Precursors to OpenJML
- OpenJDK
- OpenJML
- Related Tools
- Availability and Use
- Future Work
- References
- jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2
- SMT Solvers and SMT-LIB
- Tools and Materials
- Availability
- Future Work
- Related Tools and Materials
- References
- opaal: A Lattice Model Checker
- Introduction
- Examples
- Database Programs
- Asynchronous Lossy Communication Protocol: Leader Election
- Cache Analysis
- Timed Automata
- Conclusion
- References
- A Tabular Expression Tool box forMatlab/Simulink
- Introduction
- Related Work
- Preliminaries
- Tabular Expression
- Matlab/Simulink
- Toolbox
- Model
- Table Toolbox GUI
- Verification and Validation
- Case Study
- Conclusion and Future Work
- References
- LLVM2CSP: Extracting CSP Models from Concurrent Programs
- Introduction
- Assembling CSP Models of Concurrent Programs
- Optimizing Models for FDR
- The llvm2csp User Interface
- Functions and Variables
- Types and Arithmetics
- Conclusions
- References
- Multi-Core LTSmin: Marrying Modularity and Scalability
- LTSmin in a Nutshell
- LTSmin Multi-Core Architecture
- Multi-Core Load Balancing
- Example Use Cases
- Incremental State Hashing
- Multi-Core State Compression
- Experiments
- References
- GiNaCRA: A C++ Library for Real Algebraic Computations
- Introduction
- Real Algebra
- Featuresof GiNaCRA
- How to Use GiNaCRA
- References
- Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code
- Introduction
- Overview of Kopitiam
- Coq Editor and Goal Viewer
- The SimpleJava Programming Language
- Example Verification of Factorial
- Related Work
- Conclusion and Future Work
- References
- Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction
- Introduction
- Model Checking
- The Milestones Symbolic Model-Checker
- Modeling Language
- BDD-Based CTL Verification
- BDD-Based LTL Verification
- SAT-Based LTL Verification
- Exporting to Promela and NuSMV
- Evaluation
- Conclusion
- References
- Author Index
