【摘 要】
：
电子商务的迅速发展,使电子商务协议的开发变得十分必要,这些协议应确保信息交互的可靠性与完整性.形式化建模是设讨具有高可靠性计算机系统的有效方法,因而,对电子商务系统
论文部分内容阅读
电子商务的迅速发展,使电子商务协议的开发变得十分必要,这些协议应确保信息交互的可靠性与完整性.形式化建模是设讨具有高可靠性计算机系统的有效方法,因而,对电子商务系统的形式化分析将是非常有意义的工作.该文以一个电子报税系统为例,探讨形式化方法在电子商务协议设计上的应用.该文应用时间自动机(TA)和模型验证工具UPPAAL设计并验证了电子报税协议,通过模型验证方法,证明了系统满足税款完整性、纳税凭证完整性和报税单有效性等系统需求,为电子报税系统的可靠实现提供了形式化的论据.在研究工作中,首先,我们设计了一个用于电子报税系统的协议;然后,采用时间自动机为系统建模,并用UPPAAL对系统的上述性质进行了验证,给出了在故障情况下,保证协议正确执行的恢复机制.最后,对电子报税软件的实现作了简单介绍.
其他文献
该文以平面几何教学平台的开发设计为背景,对整个系统的结构进行了分析,并详细介绍了它所具有的功能和它们的实现方法以及在开发过程中遇到的一些问题的解决方法.文中还详细
云计算作为一种新型服务计算模式的出现,将各种各样的软硬件资源整合成不同类型服务,并且可以通过网络提供给用户使用。基础设施即服务(IaaS, Infrastructure-as-a-Service)
该论文提出的实时资源操作系统的模型包括三个部分:实时核心接口(PTKI)、实时资源接口(RTTI)和实时应用编程接口(RTAP).这种结构框架把对宿主操作系统的修改部分通过分离隐藏
一个企业或组织要想在愈加激烈的竞争中继续生存,必须能够给广泛的用户提供经济而快捷的业务信息访问,解决该问题的方案就是建立企业级的决策支持系统——数据仓库系统.数据
在知识工程中,知识表示的重要性是不言而喻的,它的质量直接影响着运行着它的系统的性能.该文进行了对基于扩展标识性语言——XML的知识表示方法的研究工作.和HTML一样,XML也
该文介绍了基于知识和数学模型的农业专家系统生成工具的设计与实现.该文主要分为四部分,分别介绍了农业专家系统生成工具的总体结构、知识库管理系统、模型库管理系统和推理
电子现金是一种新型的电子支付方式，它具有保护用户支付行为隐蔽性，防止拒绝支付和透支行为等诸多优点，它作为纸币的电子等价物已完全可能具备货币的五种基本功能，即价值量度、流
该文主要研究内容是在结点的故障模型为Fail-silent和验证性拜占庭故障的条件下,对分布式故障诊断技术中的四个关键问题进行了深入研究,包括:故障检测;信息传播;协同;故障诊
该文介绍国家高性能计算机环境(NHPCE)中资源信息管理的设计和实现.NHPCE,我们又称之为网格(GRID),其实现的软件我们称之为GRIDWARE.其中资源信息的管理和收集是GRIDWARE中一