Efficient model checking of safety properties

DOI10.1007/3-540-44829-2_5MaRDI QIDQ4426372zbMATH OpenFDO

Authors Timo Latvala

Publication date 16 September 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2648/26480074.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• On the Construction of Fine Automata for Safety Properties
• Yet another look at LTL model checking
• Efficient Büchi automata form LTL formulae
• scientific article; zbMATH DE number 2102704
• Model checking of safety properties

Cited in

(21)

• Safety property-driven stubborn sets
• On the limits of refinement-testing for model-checking CSP
• Time-constrained temporal logic control of multi-affine systems
• Time window temporal logic
• An extended framework for passive asynchronous testing
• On the Construction of Fine Automata for Safety Properties
• Falsification of LTL Safety Properties in Hybrid Systems
• Using simplex method in verifying software safety
• Modeling and Verification of High-Assurance Properties of Safety-Critical Systems
• Model Checking Safety-Critical Systems Using Safecharts
• scientific article; zbMATH DE number 2102704 (Why is no real title available?)
• scientific article; zbMATH DE number 2102708 (Why is no real title available?)
• Finite Models vs Tree Automata in Safety Verification
• Hardware and Software, Verification and Testing
• Model checking of safety properties
• Quantitative safety and liveness
• Model-based reinforcement learning for approximate optimal control with temporal logic specifications
• A mobile robot controller using reinforcement learning under scLTL specifications with uncertainties
• Verifying relative safety, accuracy, and termination for program approximations
• Asynchronous composition of LTL properties over infinite and finite traces
• Experiments with deterministic -automata for formulas of linear temporal logic

Describes a project that uses

Uses Software

• LTL2BA
• SPIN

This page was built for publication: Efficient model checking of safety properties

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