| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910809171103321 |
|
|
Autore |
Fisher Michael <1962-> |
|
|
Titolo |
An introduction to practical formal methods using temporal logic / / Michael Fisher |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Chichester, West Sussex, U.K. ; ; Hoboken, N.J., : Wiley, c2011 |
|
|
|
|
|
|
|
ISBN |
|
1-119-99146-3 |
1-283-40534-2 |
9786613405340 |
1-119-99148-X |
1-119-99147-1 |
|
|
|
|
|
|
|
|
Edizione |
[1st edition] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (710 p.) |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Temporal automata |
Logic, Symbolic and mathematical |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Description based upon print version of record. |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
|
Nota di contenuto |
|
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 Patterns |
|
|
|
|
|
|
|
|
|
|
|
7.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; Index |
|
|
|
|
|
|
Sommario/riassunto |
|
The 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 subject |
|
|
|
|
|
|
|
| |