Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications

DOI10.1007/978-3-540-75596-8_38MaRDI QIDQ3510824zbMATH OpenOpenAlexFDO

Authors Salamah Salamah, Ann Q. Gates, Steve Roach, Vladik Kreinovich

Publication date 3 July 2008

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-75596-8_38

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model Checking Software
• Formal specification generation from requirement documents
• Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models
• Automated recognition of stutter invariance of LTL formulas
• Pattern-based refinement of assume-guarantee specifications in reactive synthesis

Cites work

• Completing the temporal picture
• scientific article; zbMATH DE number 2102731 (Why is no real title available?)

Cited in

(3)

• Pattern-based and composition-driven automatic generation of logical specifications for workflow-oriented software models
• Manipulating LTL Formulas Using Spot 1.0
• Model Checking Software

This page was built for publication: Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3510824)