NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012, ProceedingsAlwyn Goodloe, Suzette Person Springer, 30.03.2012 - 466 Seiten This book constitutes the refereed proceedings of the Fourth International Symposium on NASA Formal Methods, NFM 2012, held in Norfolk, VA, USA, in April 2012. The 36 revised regular papers presented together with 10 short papers, 3 invited talks were carefully reviewed and selected from 93 submissions. The topics are organized in topical sections on theorem proving, symbolic execution, model-based engineering, real-time and stochastic systems, model checking, 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. |
Inhalt
| 1 | |
| 2 | |
| 3 | |
| 8 | |
Lessons Learnt from the Adoption of Formal ModelBased Development
| 24 |
Symbolic Execution of Communicating and Hierarchically Composed UMLRT State Machines
| 39 |
Inferring Definite Counterexamples through UnderApproximation
| 54 |
Modifying Test Suite Composition to Enable Effective PredicateLevel Statistical Debugging
| 70 |
Learning Markov Models for Stationary System Behaviors
| 216 |
The Use of Rippling to Automate EventB Invariant Preservation Proofs
| 231 |
ThreadModular Model Checking with Iterative Refinement
| 237 |
Towards LTL Model Checking of Unmodified ThreadBased C C++ Programs
| 252 |
Integrating Statechart Components in Polyglot | 267 |
Using PVS to Investigate Incidents through the Lens of Distributed Cognition
| 273 |
Automated Analysis of Parametric TimingBased Mutual Exclusion Algorithms
| 279 |
Efficient Symbolic Execution of ValueBased Data Structures for Critical Systems
| 295 |
Rigorous Polynomial Approximation Using Taylor Models in Coq
| 85 |
Enhancing the Inverse Method with State Merging
| 100 |
ClassModular ClassEscape and Pointsto Analysis for ObjectOriented Languages
| 106 |
Testing Static Analyzers with Randomly Generated Programs
| 120 |
Compositional Verification of Architectural Models | 126 |
A Safety Case Pattern for ModelBased Development Approach
| 141 |
PVS Linear Algebra Libraries for Verification of Control Software Algorithms in CACSL
| 147 |
A Controlled Language for Consistency Checking of Natural Language Temporal Requirements
| 162 |
Some Steps into Verification of Exact Real Arithmetic
| 168 |
Runtime Verification Meets Android Security | 174 |
Specification in PDL with Recursion | 181 |
An Empirical Study
| 195 |
Sound Formal Verification of Linuxs USB BP Keyboard Driver
| 210 |
Generating Verifiable Java Code from Verified PVS Specifications
| 310 |
Belief Bisimulation for Hidden Markov Models | 326 |
Abstract Model Repair | 341 |
ClosedLoop Symbolic Execution | 356 |
On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols
| 371 |
Incremental Verification with Mode Variable Invariants in State Machines
| 388 |
A Semantic Analysis of Wireless Network Security Protocols
| 403 |
Runtime Verification with Predictive Semantics | 418 |
A Case Study in Verification of Embedded Network Software
| 433 |
Checking and Distributing Statistical Model Checking | 449 |
| 464 | |
Andere Ausgaben - Alle anzeigen
NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA ... Alwyn Goodloe,Suzette Person Eingeschränkte Leseprobe - 2012 |
NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA ... Alwyn Goodloe,Suzette Person Keine Leseprobe verfügbar - 2012 |
Häufige Begriffe und Wortgruppen
AADL abstract interpretation ACSL algorithm analysis analyzed annotations application approach array atomic propositions automated automatically bisimilarity bisimulation Boolean bugs component composite Computer constraints Cousot defined definition denote error evaluation example finite formal methods formal verification framework function global Heidelberg hidden Markov model IEEE IMCs implementation initial input integer invariant iterations Java KMTS labeled language lemmas linear LLVM LNCS logic loop LTL formula Markov chains mathematical model checking model-based monitored node NuSMV operations parameters path performed points-to polynomial predicate predictive semantics predictive word proof protocol prove queue reachable relation requirements rPDL runtime satisfies Section sequence Simulink specification Springer static static analysis structure SymExe SysML Taylor models techniques theorem tool transition transition relation translation tuple updated variables verification