Paper Info
Title
Quantitative and qualitative analysis of SysML activity diagrams
Abstract
Model-driven engineering refers to a range of approaches that uses models throughout systems and software development life cycle. Towards sustaining such a successful approach in practice, we present a model-based verification framework that supports the quantitative and qualitative analysis of SysML activity diagrams. To this end, we propose an algorithm that maps SysML activity diagrams into Markov decision processes expressed using the language of the probabilistic symbolic model checker PRISM. Furthermore, we elaborate on the correctness of our translation algorithm by proving its soundness with respect to a SysML activity diagrams operational semantics that we also present in this work. The generated models can be verified against a set of properties expressed in the probabilistic computation tree logic. To automate our approach, we developed a prototype tool that interfaces a modeling environment and the probabilistic model checker. We also show how to leverage adversary generation to provide the developer with a useful counterexample/witness as a feedback on the verified properties. Finally, the established theoretical foundations are complemented with an illustrative case study that demonstrates the usability and benefit of such a framework.
Year
DOI
Venue
2014
10.1007/s10009-014-0305-6
International Journal on Software Tools for Technology Transfer (STTT)
Keywords
DocType
Volume
activity calculus,model-driven engineering,sysml activity diagrams,probabilistic verification,markov decision process
Journal
16
Issue
ISSN
Citations 
4
1433-2787
1
PageRank 
References 
Authors
0.35
27
2
Name
Order
Citations
PageRank
Yosr Jarraya117314.52
Mourad Debbabi21467144.47