Model checking XSL transformations |
| |
| Affiliation: | 1. Computer Science and System Engineering Department, ENSTA Paris Tech, 828, Boulevard des Maréchaux, 91762 Palaiseau, France;2. Embedded Systems Engineering Section, Technical University of Denmark, Richard Petersens Plads, Building 322, 2800 Lyngby, Denmark;1. Realtek Semiconductor Corp., No. 2 Innovation Rd II, Science-Based Industrial Park, Hsin-Chu, Taiwan;2. Department of Computer Science and Information Engineering, Tamkang University, New Taipei City, Taiwan;1. Key Lab of Optical Fiber Sensing and Communications, School of Communication & Information Engineering, University of Electronic Science and Technology of China, Chengdu 611731, China;2. Simula Research Laboratory, Lysaker 1325, Norway;3. Department of Computer Science and Engineering, Oakland University, Rochester, MI 48309, USA;1. Queen Mary, University of London, UK;2. University of Rijeka, HR, Croatia;3. Federal University of Paraíba, João Pessoa, Brazil;4. University of Pennsylvania, Philadelphia, USA;5. University College London, UCL-CS, UK;6. National Research University Higher School of Economics, Moscow, Russian Federation;1. College of Information Science and Engineering, Hunan University, Changsha 410082, China;2. Institute of Computing Technology, Chinese Academy of Sciences, Beijing 100190, China;1. Department of Computer Science, Yonsei University, Seodaemun-gu, Shinchon-dong 134, Seoul 120-749, Republic of Korea;2. Department of Computer Engineering, Hongik University, Mapo-gu, Sangsoo-Dong 72-1, Seoul 121-791, Republic of Korea |
| |
| Abstract: | The XSLT language is key technology to develop software which manipulates data encoded in XML, a versatile formalism widely adopted for information description and exchange. This motivates the adoption of formal techniques to certify the correctness (with respect to the expected output) and robustness (e.g., tolerance to malformed inputs) of the XSLT code. Unfortunately, such code cannot be validated using only static approaches (i.e., without executing it), due to the complexity of the XSLT formalism. In this paper we show how a software verification technology, namely the model checking, can be adapted to obtain an effective and easy to use XSLT validation framework. The core of the presented methodology is the XSLToMurphi algorithm, which is able to build a formal model of an XSLT transformation, suitable to be verified through the CMurphi tool. |
| |
| Keywords: | XML technologies XSLT language Software verification Model checking |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
