Using Coq for formal modeling and verification of timed connectors

DOI10.1007/978-3-319-74781-1_37MaRDI QIDQ4989716zbMATH OpenOpenAlexFDO

Authors Weijiang Hong, M. Nawaz, Xiyue Zhang, Yi Li, Meng Sun

Publication date 26 May 2021

Published in Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-74781-1_37

zbMATH Keywords

CoqmodelingReotimed connectorverification

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Formal Verification for Components and Connectors
• SAT-based verification for timed component connectors
• SAT-based verification for timed component connectors
• scientific article; zbMATH DE number 2242593
• Symbolic model checking for channel-based component connectors

Cited in

(4)

• Coinduction in concurrent timed systems
• Formal Verification for Components and Connectors
• SAT-based verification for timed component connectors
• Using PVS for Modeling and Verification of Probabilistic Connectors

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Using Coq for formal modeling and verification of timed connectors

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