Proceedings of the Second NASA Formal Methods SymposiumThis publication contains the proceedings of the Second NASA Formal Methods Symposium sponsored by the National Aeronautics and Space Administration and held in Washington D.C. April 13-15, 2010. Topics covered include: Decision Engines for Software Analysis using Satisfiability Modulo Theories Solvers; Verification and Validation of Flight-Critical Systems; Formal Methods at Intel -- An Overview; Automatic Review of Abstract State Machines by Meta Property Verification; Hardware-independent Proofs of Numerical Programs; Slice-based Formal Specification Measures -- Mapping Coupling and Cohesion Measures to Formal Z; How Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project; A Machine-Checked Proof of A State-Space Construction Algorithm; Automated Assume-Guarantee Reasoning for Omega-Regular Systems and Specifications; Modeling Regular Replacement for String Constraint Solving; Using Integer Clocks to Verify the Timing-Sync Sensor Network Protocol; Can Regulatory Bodies Expect Efficient Help from Formal Methods?; Synthesis of Greedy Algorithms Using Dominance Relations; A New Method for Incremental Testing of Finite State Machines; Verification of Faulty Message Passing Systems with Continuous State Space in PVS; Phase Two Feasibility Study for Software Safety Requirements Analysis Using Model Checking; A Prototype Embedding of Bluespec System Verilog in the PVS Theorem Prover; SimCheck: An Expressive Type System for Simulink; Coverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness; Software Model Checking of ARINC-653 Flight Code with MCP; Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B; Formal Verification of Large Software Systems; Symbolic Computation of Strongly Connected Components Using Saturation; Towards the Formal Verification of a Distributed Real-Time Automotive System; Slicing AADL Specifications for Model Checking; Model Checking with Edge-valued Decision Diagrams; and Data-flow based Model Analysis.
Document ID
20100018529
Acquisition Source
Langley Research Center
Document Type
Conference Proceedings
Authors
Munoz, Cesar (NASA Langley Research Center Hampton, VA, United States)
IDRelationTitle20100018543WorkVerification of Faulty Message Passing Systems with Continuous State Space in PVS20100018530WorkSynthesis of Greedy Algorithms Using Dominance Relations20100018538WorkData-Flow Based Model Analysis20100018535WorkFormal Methods at Intel - An Overview20100018545WorkSlice-Based Formal Specification Measures -- Mapping Coupling and Cohesion Measures to Formal Z20100018537WorkHow Formal Methods Impels Discovery: A Short History of an Air Traffic Management Project20100018546WorkA Machine-Checked Proof of A State-Space Construction Algorithm20100018553WorkTowards the Formal Verification of a Distributed Real-Time Automotive System20100018547WorkPhase Two Feasibility Study for Software Safety Requirements Analysis Using Model Checking20100018534WorkAutomated Assume-Guarantee Reasoning for Omega-Regular Systems and Specifications20100018532WorkDecision Engines for Software Analysis Using Satisfiability Modulo Theories Solvers20100018540WorkA Prototype Embedding of Bluespec System Verilog in the PVS Theorem Prover20100018542WorkA New Method for Incremental Testing of Finite State Machines20100018539WorkCan Regulatory Bodies Expect Efficient Help from Formal Methods?20100018552WorkFormal Verification of Large Software Systems20100018556WorkEvaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B20100018533WorkVerification and Validation of Flight-Critical Systems20100018550WorkSoftware Model Checking of ARINC-653 Flight Code with MCP20100018554WorkAutomatic Review of Abstract State Machines by Meta Property Verification20100018548WorkModeling Regular Replacement for String Constraint Solving20100018536WorkSimCheck: An Expressive Type System for Simulink20100018541WorkModel Checking with Edge-Valued Decision Diagrams20100018531WorkCoverage Metrics for Requirements-Based Testing: Evaluation of Effectiveness20100018551WorkSymbolic Computation of Strongly Connected Components Using Saturation20100018544WorkUsing Integer Clocks to Verify the Timing-Sync Sensor Network Protocol20100018549WorkSlicing AADL Specifications for Model Checking20100018555WorkHardware-Independent Proofs of Numerical Programs