Abstract: Ｂmethod is one of the formal methods, which supports the whole process of software development from the specification to code generation. This paper applies the B method to Web-based travel agency system, based on the analysis of the state representation in server and client side the formal abstract machine as well as its refinements is given.

Key words: Formal method, B method, Web technology, Abstract machine

摘要： 形式化B方法支持从规格说明到代码生成的全部软件开发过程。结合网络旅游服务系统模型，讨论了形式化B方法的具体运用，在分析服务器端和客户端状态表示的基础上，给出了该系统的抽象机模型及其精化过程。

关键词: 形式化方法, B方法, Web技术, 抽象机

CLC Number: 

• TP391