04012nam 2200613Ia 450 991080917110332120170815161710.01-119-99146-31-283-40534-297866134053401-119-99148-X1-119-99147-1(CKB)3460000000003345(EBL)698529(SSID)ssj0000477008(PQKBManifestationID)11332023(PQKBTitleCode)TC0000477008(PQKBWorkID)10501564(PQKB)10931503(MiAaPQ)EBC698529(OCoLC)729726226(CaSebORM)9780470027882(EXLCZ)99346000000000334520101207d2011 uy 0engur|n|---|||||txtccrAn introduction to practical formal methods using temporal logic[electronic resource] /Michael Fisher1st editionChichester, West Sussex, U.K. ;Hoboken, N.J. Wileyc20111 online resource (710 p.)Description based upon print version of record.0-470-02788-6 Includes bibliographical references and index.Cover; Title Page; Copyright; Preface; Chapter 1: Introduction; 1.1 Aims of the Book; 1.2 Why Temporal Logic?; 1.3 What is Temporal Logic?; 1.4 Structure of the Book; Chapter 2: Temporal Logic; 2.1 Intuition; 2.2 Syntactic Aspects; 2.3 Semantics; 2.4 Reactive System Properties; 2.5 What is Temporal Logic?; 2.6 Normal Form; 2.7 Büchi Automata and Temporal Logic; 2.8 Advanced Topics; 2.9 Final Exercises; Chapter 3: Specification; 3.1 Describing Simple Behaviours; 3.2 A Semantics of Imperative Programs; 3.3 Linking Specifications; 3.4 Advanced Topics; 3.5 Final Exercises; 3.6 Where to Next?Chapter 4: Deduction4.1 Temporal Proof; 4.2 Clausal Temporal Resolution; 4.3 The TSPASS System; 4.4 Advanced topics; 4.5 Final Exercises; Chapter 5: Model Checking; 5.1 Algorithmic Verification; 5.2 Automata-Theoretic Model Checking; 5.3 The Spin System; 5.4 Advanced Topics; 5.5 Final Exercises; Chapter 6: Execution; 6.1 From Specifications to Programs; 6.2 METATEM: Executing Temporal Formulae; 6.3 The Concurrent MetateM system; 6.4 Advanced Topics; Chapter 7: Selected Applications; 7.1 Model Checking Programs; 7.2 Security Protocol Analysis; 7.3 Recognizing Temporal Patterns7.4 Parameterized Systems7.5 Reasoning with Intervals; 7.6 Planning; Chapter 8: Summary; Appendix A: Review of Classical Logic; A.1 Introduction; A.2 Propositional Logic; A.3 Normal Forms; A.4 Propositional Resolution; A.5 Horn Clauses; A.6 First-Order Logic; Appendix B: Solutions to Exercises; B.1 Solutions: Chapter 2; Solutions: Chapter 3; Solutions: Chapter 4; Solutions: Chapter 5; Solutions: Chapter 6; Solutions: Appendix A; References; IndexThe name ""temporal logic"" may sound complex and daunting; but while they describe potentially complex scenarios, temporal logics are often based on a few simple, and fundamental, concepts - highlighted in this book. An Introduction to Practical Formal Methods Using Temporal Logic provides an introduction to formal methods based on temporal logic, for developing and testing complex computational systems. These methods are supported by many well-developed tools, techniques and results that can be applied to a wide range of systems. Fisher begins with a full introduction to the subjectTemporal automataLogic, Symbolic and mathematicalTemporal automata.Logic, Symbolic and mathematical.005.131511.3Fisher Michael1962-1654860MiAaPQMiAaPQMiAaPQBOOK9910809171103321An introduction to practical formal methods using temporal logic4006954UNINA