基于Web的形式化方法工具RRTChecker的研究与设计

Research and Design of a Web-based Formal Methods Tool:RRTChecker

形式化方法工具通常是在UNIX/Linux系统下设计开发的,难于使用阻碍了形式化方法的进一步推广。本文针对形式化方法RAISE,提出了一种研究和开发基于Web的工具的方法。该方法以原有的RAISE工具为基础,通过Shell管道拦截技术、ASP技术、ActiveX DLL技术及路径重写技术,将工具的所有功能集成整合到统一的、用户友好的Web界面上,用户可通过鼠标在浏览器中进行不同的操作。原有的RAISE工具的所有功能,在基于浏览器的集成化工具中得到全面支持。该方法也为开发其它形式化方法基于Web的工具提供了新思路。

Formal methods tools are typically developed and used in UNIX/Linux system,and the difficulties in the use of the tools prevent the formal methods from being more popularized. A method of research and design the Web-based formal methods tool for RAISE is proposed in this paper. Through the adopting of the shell pipeline interception technique,ASP,ActiveX DLL and pathname rewriting technique,the RRTChecker （RAISE Remote Type Checker） is designed as an internet application to support the usage of RAISE tools developed in UNU/IIST through internet. All the functions of the RAISE tools are integrated into a user friendly Web interface,which can be operated by mouse easily. The method proposed in this paper can be employed in the development of the Web-based tools for other formal methods.