Translating Activity Diagram from Duration Calculus for
Modeling of RealTime Systems and its Formal
Verification using UPPAAL and DiVinE
Keywords: Formal Semantics, Formal Modeling, RealTime System, Verification, UPPAAL, DiVinE
Mehran University Research Journal of Engineering & Technology
Volume 35 , Issue 1
MUHAMMAD ABDUL BASIT UR RAHIM , FAHIM ARIF , ,
References
1. 
Object Modeling Group, “Specificaiton System Modeling
Language (OMG SysML)”, Object Modeling Group, June
2012. [Online]. Available: www.omgsysml.org/INCOSEOMGSysMLTutorialFinal090901.pdf. [Accessed 28
September 2014] 
2. 
Olderog, E.R., and Dierks, H., “RealTime Systems Formal Specification and Automatic Verification”,
Cambridge University Press, New York, 2008 
3. 
Rahim, M.A.B, Arif, F., Mehmood, R., and Ahmad, J.,
“Modeling and Validation of Realtime Systems”, Design
Automation of Embedded System, pp. 18,
November, 2014 
4. 
Rahim, M.A.B., Ahmad, J., and Arif, F., “Parallel
verification of UML using DiVinE tool”, 5th
International Conference on Computer Science and
Information Technology, Amman, Jordan, 2728 March,
2013 
5. 
Rahim, M.A.B., Arif, F., and Ahmad, J., “Modeling of
Embedded System Using SysML and Its Parallel
Verification Using DiVinE Tool”, Computational Science
and Its Applications, Guimarães, pp. 541555, Portugal,
Springer, July, 2014 
6. 
Hansen, M.R., and Chaochen, Z., "Semantics and
Completeness of Duration Calculus", RealTime: Theory
in Practice, pp. 209225, The Netherland, Springer
Berlin Heidelberg, June, 1992 
7. 
Pandya, P.K., "Specifying and Deciding Quantified
DiscreteTime Duration Calculus Formulae using
DCVALID", Proceedings of RealTime Tools, Aalborg,
2000. 
8. 
Hansen M.R., Phan, A.D., and Brekling, A.W., "A
Practical Approach to Model Checking Duration Calculus
using Presburger Arithmetic", Annals of Mathematics
and Artificial Intelligence, Volume 71, Nos. 13,
pp. 251278, July, 2014. 
9. 
Guelev, D., and Hung, D.W., "Reasoning about QoS
Contracts in the Probabilistic Duration Calculus", 5th
International Workshop on Formal Foundations of
Embedded Software and ComponentBased Software
Architectures, Budapest, Hungary, June, 2010. 
10. 
Ouchani, S., Mohamed, O.A., and Debbabi, M., "A Formal
Verification Framework for SysML Activity Diagrams",
Expert Systems with Applications, Volume 41, No. 6,
pp. 27132728, May, 2014 
11. 
Ouchani, S., Mohamed, O.A., and Debbabi, M., "A
Security Risk Assessment Framework for SysML Activity
Diagrams", IEEE 7th International Conference on
Software Security and Reliability, Gaithersburg, MD,
1820 June, 2013. 
12. 
Ouchani, S., Mohamed, O.A., and Debbabi, M., "A
PropertyBased Abstraction Framework for SysML
Activity Diagrams", KnowledgeBased Systems,
Volume 56, pp. 328343, 2014. 
13. 
Ouchani, S., "A Probabilistic Verification Framework
for SysML Activity Diagrams
", Proccedings of 11th
Conference on New Trends in Software Methodologies,
Tools and Techniques, Volume 24, pp. 108, 2012. 
14. 
Rahim, M.A.B., Arif, F., and Ahmad, J., "Modeling of
RealTime Embedded Systems using SysML and its
Verification using UPPAAL and DiVinE", 5th IEEE
International Conference on Software Engineering and
Service Science, Beijing, China, June, 2014. 
15. 
Olderrod, E.R., and Dierks, H., "RealTime Systems",
Oldenburg, Cambridge University Press, 2008 
16. 
Barnat, J., Brim, L., Havel, V., Havlieek, J., Kriho, J.,
Leneo, M., Roekai, P., still, V., and Weiser, J., "DiVinE
3.0  An ExplicitState Model Checker", Computer Aided
Verification, pp. 863868, Springer, 2013. 
17. 
Rahim, M.A.B.,, Arif, F., and Ahmad, J., "Parallel
Verificaiton of UML using DiVinE Tool", 5th
International Conference on Computer Science and
Information Technology, Amman, Qatar, March, 2013. 


