I want translate AADL language to Promela for system engine model checking (e.g. SPIN). I found your article (Slicing AADL Specifications for Model Checking) about this work.can you help me about this?