Abstract
In this chapter, our main objective is to closely examine the correctness of the translation procedure proposed earlier that maps SysML activity diagrams into the input language of the probabilistic model checker PRISM . In order to provide a systematic proof , we rely on formal methods, which enable us with solid mathematical basis. To do so, four main ingredients are needed. First, we need to express formally the translation algorithm. This enables its manipulation forward deriving the corresponding proofs . Second, the formal syntax and semantics for SysML activity diagrams need to be defined. This has been proposed in the previous chapter by the means of the activity calculus language. Third, the formal syntax and semantics of PRISM input language have to be defined. Finally, a suitable relation is needed in order to compare the semantics of the diagram with the semantics of the resulting PRISM model.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
L. Aceto, W. J. Fokkink, and C. Verhoef. Structural Operational Semantics, chapter 3, pages 197–292. In Bergstra, J. A., Ponse, A., and Smolka, S. A., editors, Handbook of Process Algebra. Elsevier Science, Amsterdam, 2001.
C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Transactions on Software Engineering, 29(7):2003, 2003.
C. Baier and M. Kwiatkowska. Domain Equations for Probabilistic Processes. Mathematical Structures in Computer Science, 10(6):665–717, 2000.
F. Ciesinski and M. Größer. On Probabilistic Computation Tree Logic. In Baier C., Haverkort B., Hermanns H., Katoen J-P. and Siegle M., editors, Validation of Stochastic Systems, vol. 2925 pages 147–188, Springer, Berlin, 2004.
R. Harper. Programming in Standard ML. Online working draft, February 13, 2009.
B. Jonsson and K. G. Larsen. Specification and Refinement of Probabilistic Processes. In the Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science (LICS), Amsterdam, Holland, pages 266–277. IEEE Computer Society, 1991.
M. Kattenbelt and M. Huth. Abstraction Framework for Markov Decision Processes and PCTL via Games. Technical Report RR-09-01, Oxford University Computing Laboratory, 2009.
R. Milner. An Algebraic Definition of Simulation Between Programs. In the Proceedings of the 2nd International Joint Conference on Artificial Intelligence (IJCAI), London, UK, pages 481–489, San Francisco, CA, 1971. William Kaufmann.
G. D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, University of Aarhus, 1981.
PRISM Team. The PRISM Language – Semantics. Last Visited: March 2009.
PRISM Team. PRISM – Probabilistic Symbolic Model Checker. http://www.prismmodelchecker.org/index.php. Last Visited: September 2009.
R. Segala and N. A. Lynch. Probabilistic Simulations for Probabilistic Processes. In the Proceedings of the Concurrency Theory (CONCUR’94), pages 481–496, London, UK, 1994. Springer.
M. Y. Vardi. Branching vs. Linear Time: Final Showdown. In the Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 1–22, London, UK, 2001. Springer.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Debbabi, M., Hassaïne, F., Jarraya, Y., Soeanu, A., Alawneh, L. (2010). Soundness of the Translation Algorithm. In: Verification and Validation in Systems Engineering. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15228-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-15228-3_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15227-6
Online ISBN: 978-3-642-15228-3
eBook Packages: Computer ScienceComputer Science (R0)