Nanda, Manju.

Formal Methods for Safety and Security : Case Studies for Aerospace Applications. - 1st ed. - 1 online resource (138 pages)

Intro -- Preface -- Acknowledgements -- Contents -- About the Editors -- 1 Formal Methods-A Need for Practical Applications -- Abstract -- 1.1 Introduction -- 1.2 Error and Failures in Software Systems -- 1.3 A Paradigm Shift in Systems Engineering -- 1.4 Return on Investment -- 1.5 A Need for Case Studies -- 1.6 Paper Summary -- 1.7 Final Words -- References -- 2 Formal Methods and Tools for Safety of Critical Systems -- Abstract -- 2.1 Introduction -- 2.2 Literature Survey -- 2.2.1 Formal Methods-Based Database-Intelligent Knowledge Database (IKD) -- 2.2.2 Development of Tool Related and Tool Applicability Metrics -- 2.2.3 Development of Process Related Metrics -- 2.3 Approach -- 2.3.1 RTCA DO-178B/178C Software Development Life-Cycle -- 2.4 Conclusion and Future Scope -- Acknowledgements -- References -- 3 Taming the Enemy: Framework for Comparative Analysis of Safe String Libraries -- Abstract -- 3.1 Introduction -- 3.1.1 How Are Strings Represented in C? -- 3.1.2 Common String Issues in C -- 3.1.3 Why Are Strings in C the Way They Are? -- 3.2 Safe String Libraries -- 3.3 Related Work -- 3.4 Purpose of Work -- 3.5 Selection of Libraries -- 3.6 Selection of Parameters of Interest -- 3.7 Creation of Test Suites -- 3.8 Devising Metrics for Safe String Libraries -- 3.8.1 Metric for Functional Coverage -- 3.8.2 Metric for Bounds Protection -- 3.8.3 Performance Percentile -- 3.9 Results -- 3.9.1 Static Safe String Libraries -- 3.9.2 Dynamic Safe String Libraries -- 3.10 Conclusion -- References -- 4 Dynamic Constrained Objects for Vehicular Network Modeling -- Abstract -- 4.1 Introduction -- 4.2 Related Work -- 4.3 COB: A Constrained Object Language -- 4.4 Dynamic COB with Metric Temporal Operators -- 4.5 Vehicular Network Modeling -- 4.6 Conclusion and Future Work -- References -- 5 Adoption of Formal Methods in Software Safety Analysis. Abstract -- 5.1 Introduction -- 5.2 Work -- 5.3 Conclusion -- 6 Model-Based Safety Validation for Embedded Real-Time Systems -- Abstract -- 6.1 Introduction -- 6.2 Modeling a Safety Critical System in AADL -- 6.2.1 Error Modeling Using Annex EMV2 -- 6.2.2 Behavior Modeling Using Behavior Annex BLESS -- 6.2.3 Basic System Modeling Using AADL -- 6.3 Automatic Flight Control System: Case Study -- 6.3.1 Overview of AFCS -- 6.3.2 Error Modeling of AFCS -- 6.3.3 Behavior Modeling of AFCS -- 6.4 Safety Validation of an Embedded System -- 6.5 Derivation of Safety Parameters from AADL Models -- 6.6 Safety Validation of Flight Control System -- 6.7 Conclusion -- References -- 7 Arguing Formally About Flight Control Laws Using SLDV and NuSMV -- Abstract -- 7.1 Introduction -- 7.2 Simulink Design Verifier -- 7.3 NuSMV -- 7.4 Autopilot Mode Transition -- 7.5 Automated Validation -- 7.6 Formal Method Versus Random Tests -- 7.7 Up Down Counter -- 7.8 Conclusion -- References -- 8 Formal Methods: Techniques, Applications, Thrust Areas and Future Prospects -- Abstract -- 8.1 Introduction -- 8.2 Formal Methods -- 8.2.1 Formal Specification -- 8.2.2 Formal Verification -- 8.2.3 Formal Verification Techniques -- 8.3 Applications -- 8.3.1 Software Formal Verification -- 8.3.2 Hardware Formal Verification -- 8.4 Thrust Areas -- 8.5 Future Prospects -- 8.6 Conclusions -- References -- 9 Design Fault Identification in MBD for Safety Critical Systems -- Abstract -- 9.1 Introduction -- 9.2 Workflow -- 9.3 Validation Against Model and C Code Generation -- 9.4 Results -- 9.5 Conclusion -- References -- 10 Formal Methods Workflow for Model-Based Development -- Abstract -- 10.1 Introduction -- 10.2 V& -- V Workflow for MBD -- 10.3 V& -- V Workflow Using SLDV -- 10.3.1 V& -- V Workflow Details -- 10.3.1.1 Detecting Early Design Errors -- 10.3.1.2 Functional Verification. 10.3.1.3 Structural Coverage Analysis -- 10.3.1.4 Defect Localization -- 10.4 Conclusion -- References -- 11 Race That Never Ends! -- Abstract -- 11.1 Introduction -- 11.1.1 Terminology -- 11.1.2 Literature Survey -- 11.1.3 Purpose of This Study -- 11.2 Dynamic Race Detection -- 11.2.1 What Is Concurrency? -- 11.2.2 Properties for Race Conditions -- 11.2.3 Time-Of-Check-Time-Of-Use (TOCTOU) -- 11.2.4 What Is Dynamic Detection? -- 11.2.5 Dynamic Race Detection Techniques -- 11.2.6 Dynamic Race Detection-Disadvantages -- 11.3 Assessment Methodology -- 11.3.1 Overview of Benchmark Frameworks -- 11.3.2 Mapping CWEs to Rules (Bug Patterns) in Dynamic Analysis Tools -- 11.3.3 Analysis of Tools -- 11.3.4 Metrics and Metrics Calculation -- 11.3.5 Description of Dynamic Analysis Tools Used -- 11.3.6 Experimental Setup -- 11.4 Analysis of Tool Results -- 11.5 Comparisons of Tool Assessment Results-Dynamic Analysis and Static Analysis -- 11.6 Secure Design and Coding Guidelines -- 11.7 Conclusion -- References -- Index.

9789811041211


Software engineering.


Electronic books.

TL1-4050

629.10285