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. |
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. |
| 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 Component-Based 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. 2713-2728, 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,
18-20 June, 2013. |
| 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. |
| |
|
|