A formal verification technique for behavioural model-to-model transformations

DOI10.1007/s00165-017-0437-zzbMath1380.68286OpenAlexW2763640514MaRDI QIDQ682361

Sander de Putter, Anton Wijs

Publication date: 2 February 2018

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

Full work available at URL: https://doi.org/10.1007/s00165-017-0437-z

zbMATH Keywords

branching bisimulationexplicit-state model checkingmodel transformation verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

To compose, or not to compose, that is the question: an analysis of compositional state space generation, Unnamed Item

Uses Software

• Coq
• PRISM
• mCRL2
• CADP
• Rodin
• GPU-PRISM
• REFINER

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The existence of refinement mappings
• On the computational complexity of dynamic graph problems
• An \(O(m\log n)\) algorithm for stuttering equivalence and branching bisimulation
• A compositional proof system on a category of labelled transition systems
• Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique
• Partial Model Checking using Networks of Labelled Transition Systems and Boole an Equation Systems
• Towards Automatic Verification of Behavior Preservation for Model Transformation via Invariant Checking
• CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
• Property Preserving Refinement for Csp-Casl
• Specification and Verification of Graph-Based Model Transformation Properties
• Graph Transformation in Constant Time
• Refined Interfaces for Compositional Verification
• Branching time and abstraction in bisimulation semantics
• Sparsification—a technique for speeding up dynamic graph algorithms
• An Overview of the mCRL2 Toolset and Its Recent Advances
• Efficient Property Preservation Checking of Model Refinements
• Towards Verifying Model Transformations
• An Incremental Bisimulation Algorithm
• Formal Modeling and Analysis of Timed Systems
• Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets