Model checking action system refinements

DOI10.1007/S00165-007-0053-4MaRDI QIDQ1019017zbMATH OpenOpenAlexFDO

Authors Graeme Smith, Kirsten Winter

Publication date 27 May 2009

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-007-0053-4

zbMATH Keywords

model checkingrefinementCTLaction systems

Mathematics Subject Classification ID

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

Recommendations

• Model Checking for Action Abstraction
• Model checking for action-based logics
• Action-based model checking: logic, automata, and reduction
• scientific article; zbMATH DE number 849930
• Model checking techniqes for the analysis of reactive systems
• scientific article; zbMATH DE number 910719
• Model checking
• Model checking parameterized systems

Cites work

• scientific article; zbMATH DE number 1615985 (Why is no real title available?)
• scientific article; zbMATH DE number 140256 (Why is no real title available?)
• scientific article; zbMATH DE number 2079995 (Why is no real title available?)
• scientific article; zbMATH DE number 1487740 (Why is no real title available?)
• scientific article; zbMATH DE number 1409638 (Why is no real title available?)
• A state-based approach to communicating processes
• Model-checking CSP-Z: Strategy, tool support and industrial application
• Process simulation and refinement
• The B-Book
• Using the Alloy analyzer to verify data refinement in Z
• Verifying data refinements using a model checker

Cited in

(10)

• Action systems in incremental and aspect-oriented modeling
• Compositional action system refinement
• scientific article; zbMATH DE number 1670558 (Why is no real title available?)
• Towards the hierarchical verification of reactive systems
• Performance analysis of probabilistic action systems
• Model Checking for Action Abstraction
• Model checking simulation rules for linearizability
• scientific article; zbMATH DE number 1953035 (Why is no real title available?)
• Model checking downward simulations
• Compositional action system derivation using enforced properties

Describes a project that uses

Uses Software

• Z
• ProB

This page was built for publication: Model checking action system refinements

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