网上证券交易系统的时序Petri网描述及验证 |
| |
引用本文: | 杜玉越,蒋昌俊.网上证券交易系统的时序Petri网描述及验证[J].软件学报,2002,13(8):1698-1704. |
| |
作者姓名: | 杜玉越 蒋昌俊 |
| |
作者单位: | 1. 同济大学,计算机科学与工程系,上海,200092;聊城师范学院,计算机科学系,山东,聊城,252059;中国科学院,软件研究所,计算机科学重点实验室,北京,100080 2. 同济大学,计算机科学与工程系,上海,200092 |
| |
基金项目: | 国家自然科学基金资助项目(69973029,69933020);国家重点基础研究规划973资助项目(G1998030604);中国科学院软件研究所计算机科学重点实验室资助项目(SYSKF0205) |
| |
摘 要: | 基于时序Petri网对我国现行网上静态和动态证券交易系统进行了模拟、形式描述及功能正确性验证.应用时序逻辑推理规则,从形式上严格证明了证券交易系统需求规范及其时序Petri网模型动态行为的一致性.结果表明,时序Petri网能够清楚而简单地描述事件间的因果关系和时序关系以及并发系统中某些与时间有关的重要性质,如最终性和公平性.因此,时序Petri网可作为并发系统形式化描述和分析的有力工具.
|
关 键 词: | 模型检查 证券交易系统 时序逻辑 Petri网 形式描述 正确性验证 电子商务 |
文章编号: | 1000-9825/2002/13(08)1698-07 |
收稿时间: | 2001/7/10 0:00:00 |
修稿时间: | 2001年7月10日 |
本文献已被 CNKI 维普 万方数据 等数据库收录! |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|