Model-based construction and verification of critical systems using composition and partial refinement

DOI10.1007/S10703-010-0106-9MaRDI QIDQ633296zbMATHOpenAlexFDO

Authors Ralph D. Jeffords, Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard

Publication date 31 March 2011

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

Full work available at URL https://doi.org/10.1007/s10703-010-0106-9

zbMATH Keywords

fault-tolerancecompositionrefinementtheorem provingmaskingformal specificationproof rules

Mathematics Subject Classification ID

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

Recommendations

• An Approach to Modelling and Verification of Component Based Systems
• Verification of component-based system using model checking
• Compositional Verification for Component-Based Systems and Application
• Modeling and Verification of High-Assurance Properties of Safety-Critical Systems
• A compositional approach to the verification of hybrid systems
• Compositional Model Checking of Concurrent Systems
• A framework for the functional verification of SystemC models

Cites work

• scientific article; zbMATH DE number 1629964 (Why is no real title available?)
• scientific article; zbMATH DE number 1696500 (Why is no real title available?)
• scientific article; zbMATH DE number 526071 (Why is no real title available?)
• scientific article; zbMATH DE number 1955918 (Why is no real title available?)
• Abstract State Machines
• Aspect Categories and Classes of Temporal Properties
• Defining liveness
• Engineering and theoretical underpinnings of retrenchment
• Formally verifying fault tolerant system designs
• Mechanical Verification of Automatic Synthesis of Fault-Tolerant Programs
• Statecharts: a visual formalism for complex systems
• Synthesis of fault-tolerant concurrent programs
• The existence of refinement mappings
• Transformation of programs for fault-tolerance

Cited in

(3)

• Simulation relations for fault-tolerance
• A framework for the functional verification of SystemC models
• An Approach to Modelling and Verification of Component Based Systems

Describes a project that uses

Uses Software

• Salsa

This page was built for publication: Model-based construction and verification of critical systems using composition and partial refinement

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