SMT-based scenario verification for hybrid systems

DOI10.1007/s10703-012-0158-0zbMath1284.03216OpenAlexW1965965053WikidataQ62041178 ScholiaQ62041178MaRDI QIDQ2441772

Alessandro Cimatti, Stefano Tonetta, Sergio Mover

Publication date: 28 March 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-012-0158-0

zbMATH Keywords

message sequence chartsbounded model checkingk-inductionnetwork of hybrid automataSMT-based verification

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Temporal logic (03B44) Computation over the reals, computable analysis (03D78)

Related Items (9)

Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration ⋮ Abstractions Refinement for Hybrid Systems Diagnosability Analysis ⋮ SMT-based scenario verification for hybrid systems ⋮ SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata ⋮ Syntax-guided synthesis for lemma generation in hardware model checking ⋮ ModelPlex: verified runtime validation of verified cyber-physical system models ⋮ Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration ⋮ Zone-based verification of timed automata: extrapolations, simulations and what next? ⋮ Abstraction-based incremental inductive coverability for Petri nets

Uses Software

• HySAT
• TASS
• HyTech
• NuSMV
• MathSAT
• HyDI

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Exploiting step semantics for efficient bounded model checking of asynchronous systems
• Scenario-based verification of real-time systems using UPPAAL
• HySAT: An efficient proof engine for bounded model checking of hybrid systems
• Interpreting message flow graphs
• SMT-based scenario verification for hybrid systems
• Towards a Notion of Unsatisfiable Cores for LTL
• On the Notion of Vacuous Truth
• Matching Scenarios with Timing Constraints
• Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
• Bounded LTL model checking with stable models
• Automata and Logics for Timed Message Sequence Charts
• Verification, Model Checking, and Abstract Interpretation
• Computer Aided Verification
• LSCs: Breathing life into message sequence charts

This page was built for publication: SMT-based scenario verification for hybrid systems