Mehran University Research Journal Of Engineering &
Technology (HEC Recognized In Category "X")
Publishing Since 1982.



For Authors
For Readers
Article Information  
Translating Activity Diagram from Duration Calculus for Modeling of Real-Time Systems and its Formal Verification using UPPAAL and DiVinE

Keywords: Formal Semantics, Formal Modeling, Real-Time 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/INCOSEOMGSysML-Tutorial-Final-090901.pdf. [Accessed 28 September 2014]
2. Olderog, E.R., and Dierks, H., “Real-Time 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 Real-time 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, 27-28 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. 541-555, Portugal, Springer, July, 2014
6. Hansen, M.R., and Chaochen, Z., "Semantics and Completeness of Duration Calculus", Real-Time: Theory in Practice, pp. 209-225, The Netherland, Springer Berlin Heidelberg, June, 1992
7. Pandya, P.K., "Specifying and Deciding Quantified Discrete-Time Duration Calculus Formulae using DCVALID", Proceedings of Real-Time Tools, Aalborg, 2000.
8. 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, 18-20 June, 2013.
9. 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. 1-3, pp. 251-278, July, 2014.
10. 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 Component-Based Software Architectures, Budapest, Hungary, June, 2010.
11. 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. 2713-2728, May, 2014
12. Ouchani, S., Mohamed, O.A., and Debbabi, M., "A Property-Based Abstraction Framework for SysML Activity Diagrams", Knowledge-Based Systems, Volume 56, pp. 328-343, 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 Real-Time 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., "Real-Time 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 Explicit-State Model Checker", Computer Aided Verification, pp. 863-868, 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.