Umfang:
Online-Ressource (X, 361 S.)
Ausgabe:
Online-Ausg. 2007 Springer eBook collection. Computer science Electronic reproduction; Available via World Wide Web
ISBN:
9783540709527
Serie:
Lecture notes in computer science 4346
Anmerkung:
Includes bibliographical references and index
,
""Title page""; ""Preface""; ""Organization""; ""Table of Contents""; ""Challenges for Formal Verification in IndustrialSetting""; ""Introduction""; ""Our Approach to Formal Verification of FP Arithmetic""; ""FORTE System and STE""; ""Pre- and Post-condition Framework""; ""Managing the Size of BDDs""; ""Verification Methodology""; ""Verification of Fused Multiply-Add""; ""Floating-Point Multiply-Add""; ""Verification of Multiplier""; ""Verification of Adder and Rounder""; ""Debugging""; ""Our Impact on the Design Project""; ""Proof Management""; ""Summary""
,
""Distributed Verification:Exploring the Power of Raw Computing Power""""Brute-Force in Distribute Verification""; ""Algorithms for Accepting Cycle Detection""; ""Maximal Accepting Predecessor (MAP)""; ""Eliminating Bad States (OWCTY)""; ""Maximal Number of Accepting Predecessors (NEGC)""; ""Back-Level Edges (BLEDGE)""; ""Comparing the Algorithms""; ""Conclusions""; ""An Easy-to-Use, Efficient Tool-Chain to Analyzethe Availability of TelecommunicationEquipment""; ""Introduction""; ""Tool Chain""; ""Model World""; ""OpenSESAME Input Model""; ""Properties of High-Level MRMs""
,
""Symbolic Representation and Solution of MRMs""""Symbolic Representation of Low-Level Markov Reward Models""; ""Generating and Solving the Low-Level Markov Reward Model""; ""Case Study: Fault-Tolerant Adjunct Processor""; ""System Description""; ""Model Evaluation""; ""Conclusion""; ""“To Store or Not To Store� Reloaded:Reclaiming Memory on Demand""; ""Introduction""; ""Safe Lossy Hashing""; ""Selecting Victim States to Swap Out""; ""Single-Successor States""; ""Bloom-Filter Cache""; ""Implementation""; ""The Life-Cycle of States""; ""Speedups Through I/O Reduction""
,
""Partitioning the Closed Set""""Hash Compaction""; ""Compression""; ""Results""; ""Related Work""; ""Conclusions""; ""Discovering Symmetries""; ""Introduction""; ""Motivating Application""; ""An Illustrative Example""; ""Defining Symmetry""; ""Generalized Invariance Groups""; ""Computing Symmetries""; ""Property-Based Permutations""; ""Exploiting Dependencies""; ""Refining Symmetries""; ""An Algorithm for Computing Symmetries""; ""Experimentation""; ""Discussion""; ""References""; ""On Combining Partial Order Reduction withFairness Assumptions""; ""Introduction""
,
""Conclusion and Further Work""""Related Work""; ""Case Study: The MPEG Decoder System""; ""Conjoint Generation of Schedulings and Timings""; ""The SystemC Models We Consider""; ""Main Ideas""; ""The Temporal Constraints""; ""The Algorithm""; ""Elements for the Correctness of the Algorithm""; ""Relationships for Partial Order Reduction Techniques""; ""Representation of the SUTD""; ""Relationships""; ""Generation of Schedulings""; ""SystemC, Scheduling Problems, and Loose Timings""; ""The SystemC Scheduler""; ""Examples with Fixed Durations""; ""Examples with Loose Durations""
,
""Introduction""
,
Electronic reproduction; Available via World Wide Web
Weitere Ausg.:
ISBN 9783540709510
Weitere Ausg.:
Erscheint auch als Druck-Ausgabe Formal Methods : Applications and Technology : 11th International Workshop, FMICS 2006 and 5th International Workshop, PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006 : Revised Selected Papers
Sprache:
Englisch
Fachgebiete:
Informatik
Schlagwort(e):
Softwareentwicklung
;
Zuverlässigkeit
;
Fehlertoleranz
;
Formale Methode
;
Programmverifikation
;
Softwarespezifikation
;
Sicherheitskritisches System
;
Eingebettetes System
;
Konferenzschrift
DOI:
10.1007/978-3-540-70952-7
URL:
Volltext
(lizenzpflichtig)
