A formal verification technique for behavioural model-to-model transformations
type: Item
instance of: scholarly article
title: A formal verification technique for behavioural model-to-model transformations
zbMATH Open document ID: 1380.68286
author: Sander de Putter
author: Anton Wijs
published in: Formal Aspects of Computing
publication date: 2018-02-02T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 6833745
zbMATH Keywords: model transformation verification
zbMATH Keywords: explicit-state model checking
zbMATH Keywords: branching bisimulation
describes a project that uses: Coq
describes a project that uses: PRISM
describes a project that uses: mCRL2
describes a project that uses: Rodin
describes a project that uses: GPU-PRISM
describes a project that uses: CADP
describes a project that uses: REFINER
MaRDI profile type: Publication
full work available at URL: s00165-017-0437-z
OpenAlex ID: W2763640514
cites work: The existence of refinement mappings
cites work: Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets
cites work: CTL-property transformations along an incremental design process
cites work: Q5322945
cites work: An Overview of the mCRL2 Toolset and Its Recent Advances
cites work: Graph Transformation in Constant Time
cites work: Sparsification—a technique for speeding up dynamic graph algorithms
cites work: Formal Modeling and Analysis of Timed Systems
cites work: Towards Automatic Verification of Behavior Preservation for Model Transformation via Invariant Checking
cites work: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
cites work: Q4942013
cites work: An \(O(m\log n)\) algorithm for stuttering equivalence and branching bisimulation
cites work: A compositional proof system on a category of labelled transition systems
cites work: Partial model checking using networks of labelled transition systems and Boolean equation systems
cites work: Property Preserving Refinement for Csp-Casl
cites work: Refined Interfaces for Compositional Verification
cites work: Towards Verifying Model Transformations
cites work: Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique
cites work: On the computational complexity of dynamic graph problems
cites work: An Incremental Bisimulation Algorithm
cites work: Specification and Verification of Graph-Based Model Transformation Properties
cites work: Branching time and abstraction in bisimulation semantics
cites work: Efficient Property Preservation Checking of Model Refinements
DOI: 10.1007/S00165-017-0437-Z
description: scientific article; zbMATH DE number 6833745