An Introduction to Practical Formal Methods Using Temporal Logic

DOI10.1002/9781119991472zbMath1250.68003OpenAlexW1608490958WikidataQ98283533 ScholiaQ98283533MaRDI QIDQ2996923

No author found.

Publication date: 4 May 2011

Full work available at URL: https://doi.org/10.1002/9781119991472

zbMATH Keywords

formal specificationmodel checkingsemanticsdeductionBüchi automataautomata-based model checking in SPINseparated normal formTSPASS tool

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Related Items (6)

A two-level approach based on model checking to support architecture conformance checking ⋮ Invariant-free clausal temporal resolution ⋮ Theorem proving using clausal resolution: from past to present ⋮ Dynamic logic assigned to automata ⋮ Guest editors' preface to special issue on interval temporal logics ⋮ Compositional reasoning using intervals and time reversal

Uses Software

• SLAM
• TSPASS
• METATEM
• TeMP
• Unnamed Item
• Unnamed Item

This page was built for publication: An Introduction to Practical Formal Methods Using Temporal Logic