A formal verification technique for behavioural model-to-model transformations
From MaRDI portal
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Recommendations
- Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique
- Towards verifying model transformations
- On the Specification and Verification of Model Transformations
- Towards automatic verification of behavior preservation for model transformation via invariant checking
- A model-based development approach for model transformations
Cites work
- A compositional proof system on a category of labelled transition systems
- An \(O(m\log n)\) algorithm for stuttering equivalence and branching bisimulation
- An Incremental Bisimulation Algorithm
- An overview of the mCRL2 toolset and its recent advances
- Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets
- Branching time and abstraction in bisimulation semantics
- CADP 2010: a toolbox for the construction and analysis of distributed processes
- CTL-property transformations along an incremental design process
- Efficient property preservation checking of model refinements
- Formal Modeling and Analysis of Timed Systems
- Graph Transformation in Constant Time
- scientific article; zbMATH DE number 1418456 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- On the computational complexity of dynamic graph problems
- Partial model checking using networks of labelled transition systems and Boolean equation systems
- Property Preserving Refinement for Csp-Casl
- Refined Interfaces for Compositional Verification
- Sparsification—a technique for speeding up dynamic graph algorithms
- Specification and verification of graph-based model transformation properties
- The existence of refinement mappings
- Towards automatic verification of behavior preservation for model transformation via invariant checking
- Towards verifying model transformations
- Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique
Cited in
(9)- A system for deduction-based formal verification of workflow-oriented software models
- To compose, or not to compose, that is the question: an analysis of compositional state space generation
- Verification of compliance for multilevel models in individual trace semantics
- Verification of system level model transformations
- Towards automatic verification of behavior preservation for model transformation via invariant checking
- On the Specification and Verification of Model Transformations
- scientific article; zbMATH DE number 1790353 (Why is no real title available?)
- scientific article; zbMATH DE number 7243676 (Why is no real title available?)
- Towards verifying model transformations
This page was built for publication: A formal verification technique for behavioural model-to-model transformations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q682361)
