Towards verifying model transformations

DOI10.1016/J.ENTCS.2008.04.041MaRDI QIDQ5404179zbMATH OpenOpenAlexFDO

Authors Anantha Narayanan, Gabor Karsai

Publication date 21 March 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2008.04.041

zbMATH Keywords

verificationbisimulationgraph transformation

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)

Recommendations

• On the Specification and Verification of Model Transformations
• A formal verification technique for behavioural model-to-model transformations
• Towards automatic verification of behavior preservation for model transformation via invariant checking
• A model-based development approach for model transformations
• A framework for model transformation verification

Cites work

• scientific article; zbMATH DE number 3827245 (Why is no real title available?)
• scientific article; zbMATH DE number 2016088 (Why is no real title available?)
• Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker
• Statecharts: a visual formalism for complex systems

Cited in

(16)

• Ensuring correctness of model transformations while remaining decidable
• Verification of system level model transformations
• A formal verification technique for behavioural model-to-model transformations
• Variability-based model transformation: formal foundation and application
• A framework for model transformation verification
• Testing-based translation validation of generated code in the context of IEC 61508
• Correct transformation: from object-based graph grammars to PROMELA
• Towards automatic verification of behavior preservation for model transformation via invariant checking
• Formal Methods in Computer-Aided Design
• Towards lightweight checks for mass maintenance transformations
• Model-Driven Monitoring: An Application of Graph Transformation for Design by Contract
• On the Specification and Verification of Model Transformations
• Using source transformation to test and model check implicit-invocation systems
• Combining termination proofs in model transformation systems
• Behavior Preservation in Model Refactoring Using DPO Transformations with Borrowed Contexts
• Behavior-Preserving Simulation-to-Animation Model and Rule Transformations

Describes a project that uses

Uses Software

• CheckVML
• Fujaba
• SPIN
• PROGRES

This page was built for publication: Towards verifying model transformations

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