Hou Honglun
College of Intenet of Things Engineering, Hohai University, 213022, Changzhou, China
Lv Jia
Department of Computer Science and Engineering, Zhejiang University City College, 310015, Hangzhou, China
Wu Minghui
College of Intenet of Things Engineering, Hohai University, 213022, Changzhou, China
ABSTRACT
Due to the dynamic language features, it is very difficult to verify the correctness of dynamic programs statically. In this study, we introduce a new method named soft verification, which combines static verification and dynamic run-time checking. The dynamic programs are divided into two parts: static components and dynamic components. Static components will be verified statically and dynamic components will be inserted into run-time checks, which will be executed at run-time to ensure the correctness of dynamic programs. We also use open temporal logic to specify the correctness of dynamic programs.
PDF References Citation
How to cite this article
Hou Honglun, Lv Jia and Wu Minghui, 2013. Soft Verifying Dynamic Features in Dynamic Programs. Information Technology Journal, 12: 8116-8122.
DOI: 10.3923/itj.2013.8116.8122
URL: https://scialert.net/abstract/?doi=itj.2013.8116.8122
DOI: 10.3923/itj.2013.8116.8122
URL: https://scialert.net/abstract/?doi=itj.2013.8116.8122
REFERENCES
- Clarke, E.M. and E.A. Emerson, 1981. Design and synthesis of synchronization skeletons using branching time temporal logic. Logics Programs, 131: 52-71.
CrossRefDirect Link - Clarke, E.M., E.A. Emerson and A.P. Sistla, 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., 8: 244-263.
CrossRef - Emerson, E.A. and E.M. Clarke, 1980. Characterizing Correctness Properties of Parallel Programs Using Fixpoints. In: Automata, Languages and Programming: The Seventh Colloquium Noordwijkerhout, the Netherlands July 14-18, 1980, De Bakker, J. and J. van Leeuwen (Eds.). Springer-Verlag, Berlin, Germany, pp: 169-181.
- Jonsson, B. and T. Yih-Kuen, 1996. Assumption/guarantee specifications in linear-time temporal logic. Theor. Comput. Sci., 167: 47-72.
CrossRef - Katz, E. and S. Katz, 2008. Incremental analysis of interference among aspects. Proceedings of the 7th workshop on Foundations of Aspect-Oriented Languages, April 1, 2008, Brussels, Belgium, 29-38.
CrossRef - Khatchadourian, R., J. Dovland and N. Soundarajan, 2008. Enforcing behavioral constraints in evolving aspect-oriented programs. Proceedings of the 7th workshop on Foundations of Aspect-Oriented Languages, April 1, 2008, Brussels, Belgium, pp: 19-28.
CrossRef - Khatchadourian, R. and N. Soundarajan, 2007. Rely-guarantee approach to reasoning about aspect-oriented programs. Proceedings of the 5th Workshop on Software Engineering Properties of Languages and Aspect Technologies, March 12-16, 2007, Vancouver, British Columbia, Canada,.
CrossRef - Lv., J., J. Ying, M.H. Wu, T. Jiang and F.W. Zhu, 2009. Verifying aspect-oriented programs using open temporal logic. Proceedings of the 3rd IEEE International Conference on Secure Software Integration and Reliability Improvement, July 8-10, 2009, Shanghai, China, pp: 85-92.
CrossRef - Pasareanu, C.S., M.B. Dwyer and M. Huth, 1999. Assume-guarantee model checking of software: A comparative case study. Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, July 5, 1999, Trento, Italy, pp: 168-183.
CrossRef - Xu, Q., W.P. de Roever and J. He, 1997. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects Comput., 95: 149-174.
CrossRef - Zhang, J. and B.H.C. Cheng, 2006. Using temporal logic to specify adaptive program semantics. J. Syst. Software, 79: 1361-1369.
CrossRef - Zhang, J., H.J. Goldsby and B.H. Cheng, 2009. Modular verification of dynamically adaptive systems. Proceedings of the 8th ACM International Conference on Aspect-Oriented Software Development, March 2-6, 2009, Virginia, USA, pp: 161-172.
CrossRef