Towards automated software model checking using graph transformation systems and bogor

DOI10.1631/JZUS.A0820415MaRDI QIDQ1049792zbMATH OpenOpenAlexFDO

Authors Vahid Rafe, Adel T. Rahmani

Publication date 13 January 2010

Published in Journal of Zhejiang University. Science A (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1631/jzus.a0820415

zbMATH Keywords

verificationgraph transformationsoftware model checkingattributed graph grammarsBogor

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Graph Transformations
• Explicit State Model Checking for Graph Grammars
• The Verigraph system for graph transformation
• Sound and complete abstract graph transformation
• Inductive invariant checking with partial negative application conditions

Cites work

• scientific article; zbMATH DE number 2006492 (Why is no real title available?)
• scientific article; zbMATH DE number 2016064 (Why is no real title available?)
• scientific article; zbMATH DE number 2016090 (Why is no real title available?)
• Analysis of UML Activities Using Dynamic Meta Modeling
• Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker
• CONCUR 2004 - Concurrency Theory
• Formal Analysis of Workflows Using UML 2.0 Activities and Graph Transformation Systems
• Formal verification of object-oriented graph grammars specifications
• Global Computing
• Graph Transformations
• Handbook of Graph Grammars and Computing by Graph Transformation
• Joint optimization and reachability analysis in graph transformation systems with time
• On the Use of Alloy to Analyze Graph Transformation Systems
• Towards attributed graphs in Groove (work in progress)
• Verification of distributed object-based systems.

Cited in

(8)

• Graph Transformations
• Specification and verification of graph-based model transformation properties
• Explicit State Model Checking for Graph Grammars
• Efficient symbolic implementation of graph automata with applications to invariant checking
• The Verigraph system for graph transformation
• Inductive invariant checking with partial negative application conditions
• Towards the automated generation of consistent, diverse, scalable and realistic graph models
• On the Use of Alloy to Analyze Graph Transformation Systems

Describes a project that uses

Uses Software

• GROOVE
• CheckVML
• vUML
• Bogor
• SPIN

This page was built for publication: Towards automated software model checking using graph transformation systems and bogor

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