In my research I want to theoretically prove that the model transformation is correct. Specifically, it is to verify the model transformation of a state machine model to a fault tree model.Now my idea is to find a formal language description model element and use the theorem prover for analysis and verification.But how to determine which formal language and theorem prover should I use to verify the correctness of the model transformation is a problem.I hope that the experts in the research field can give me some advice and suggestions.You can follow my ideas or give some new comments, thank you！
Hello,
Based on both models, the one to be transformed and its image resulting from the transformation, they should equivalent. That means you have to prove that the relation between both models is an equivalence relation.
This may help.
https://spectrum.library.concordia.ca/977746/1/Ouchani_Phd_F2013.pdf
Hello,
You should describe the source model (state machine), the target model ( fault tree ) and the transformation itself using a theorem prover like Isabelle/HOL or Coq. After that, you need to define some properties of this transformation and prove their correctness using the theorem prover.
- Badges
- Science topic
- Similar topics
- Biological Science
- Zoology
- Invertebrate Zoology
- Arthropods
- Insects