A formal verification technique for behavioural model-to-model transformations
From MaRDI portal
Publication:682361
DOI10.1007/s00165-017-0437-zzbMath1380.68286OpenAlexW2763640514MaRDI QIDQ682361
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
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
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
