形式化模型
形式化模型的相关文献在1989年到2022年内共计148篇,主要集中在自动化技术、计算机技术、铁路运输、测绘学
等领域,其中期刊论文114篇、会议论文22篇、专利文献705829篇;相关期刊67种,包括信息系统工程、管理观察、中国学术期刊文摘等;
相关会议19种,包括2013年全国理论计算机科学学术年会、第十四届全国Petri 网理论与应用学术年会、2012年第三届中国计算机学会服务计算学术会议等;形式化模型的相关文献由398位作者贡献,包括黄俊、韩玲莉、马恒太等。
形式化模型—发文量
专利文献>
论文:705829篇
占比:99.98%
总计:705965篇
形式化模型
-研究学者
- 黄俊
- 韩玲莉
- 马恒太
- 关永
- 唐郑熠
- 孙士勇
- 宋文
- 张大年
- 张政童
- 张楠
- 张芮
- 张苓
- 施智平
- 朱迎春
- 李必信
- 李志明
- 李晓娟
- 李欣欣
- 李正茂
- 杨春燕
- 汪彩梅
- 王燕芩
- 王瑞
- 王见思
- 王金水
- 胡文瑜
- 董磊
- 蒋忠远
- 薛醒思
- 薛锦云
- 陈昊鹏
- 黄子昂
- 黄雨
- Deng Mengmeng
- FU JianMing
- Guo Feng
- HE Fan
- JIA Xiang-Yang
- JIANG Cao-Qing
- JIANG Dong-ming
- LI Lei
- Li Bixin
- Li Zonghua
- TAN Qing-ping
- WEN Jing
- XU MingDi
- XUE Jin-yun
- YAN Fei
- YANG Yang
- YING Shi
-
-
苏霞;
张晶晶;
孙静
-
-
摘要:
由于已有方法未能使用形式化模型,导致安全协议验证效率下降,安全协议验证错误率和开销增加。结合形式化模型,提出一种基于形式化模型的电力信息审计系统安全协议验证方法。通过形式化模型,对电力信息审计系统进行形式化研究,采用SPIN和AVISPA对电力信息审计系统安全协议进行改进。利用Promela和HLPSL进行建模,查找安全协议中存在的攻击,获取攻击者的相关信息,查看存在的漏洞,完成电力信息审计系统安全协议验证。仿真实验结果表明,所提方法能够有效提升安全协议验证效率,降低安全协议验证错误率和开销。
-
-
刘琴;
王德军;
王潇潇;
郑绪睿;
孟博
-
-
摘要:
从计算机科学的角度对法律合约与智能合约的一致性研究现状进行了总结和分析.首先,分别对法律合约描述语言和智能合约开发语言进行了分类和分析,总结了每种语言的特点;其次,根据合同自动化执行的三个发展阶段对法律合约和智能合约的一致性内涵进行了分析和讨论;分别基于形式化模型和合约模板总结了由法律合约生成智能合约代码的方法和关键技术,并对其进行了讨论和评价;最后,对未来法律合约与智能合约的一致性研究进行了总结和展望.
-
-
-
-
-
-
-
-
-
-
陈晨;
刘楠;
陈卫红;
祝跃飞
- 《2010年第四届中国可信计算与信息安全学术会议》
| 2010年
-
摘要:
构建一个安全电子交易的形式化模型,为实现对相关安全协议的自动化分析提供了理论基础和技术手段.该模型基于项重写理论进行构建,通过符号化和规则化的方式刻画电子交易的3个主要过程,不但体现交易双方能互相检验身份的安全机制,并且通过项重写系统终止性和会聚性的性质证明该模型具有完整性和一致性等特点,在安全性分析方面验证该模型满足认证性和发送非否认性.
-
-
邓红艳;
翟仁健
- 《第六届全国地图学与GIS学术研讨会》
| 2008年
-
摘要:
自动制图综合质量问题已经成为其发展过程中亟需解决的重要难题,其中包括两个重要步骤:一是对自动制图综合结果的评价;二是利用质量来进行自动制图综合的过程控制.要解决这两个问题,形式化描述是第一步.本文通过对自动制图综合质量评价过程的分析,利用数学方法建立了相应的形式化模型.
-
-
-
-
-
刘晓芹;
陈星;
吕晓明;
王宝龙
- 《武器装备综合保障信息化技术研讨会》
| 2009年
-
摘要:
针对单故障诊断模型失效情况,通过对多故障诊断问题的分析研究,建立了多故障诊断的形式化模型,给出了基于相关性矩阵和双层与或关系图的多故障诊断方法,并总结了该方法的一般算法原理。本文还通过系统实例介绍了该方法的具体应用,并通过多故障诊断的结果验证了该方法。
-
-
- 《2008年(第十届)中国科协年会》
| 2008年
-
摘要:
指挥Agent具有自主性、反应性、社会性等特点,将多Agent技术及Petri网描述和分析工具引入对指挥Agent的研究中.对现有的面向Agent的Petri网进行了改进,由原来的14元组改进为16元组,重点完善了指挥Agent的内部结构模型,较为管观地揭示了各功能模块间的作用关系.并以改进的AOPN为基础,深入分析了指挥Agent的具体行为过程;建立了单个指挥Agent行为过程的形式化模型,构建了由多个指挥Agent组成的指挥控制系统的体系结构模型,探讨了令牌消息的传递机制,并采用KQML语言简要分析了消息传递实现的方法.
-
-
JIANG Cao-Qing;
蒋曹清;
YING Shi;
应时;
WEN Jing;
文静;
JIA Xiang-Yang;
贾向阳;
王一兵
- 《2012年第三届中国计算机学会服务计算学术会议》
| 2012年
-
摘要:
异常处理的可终止性是确保其正确性的重要基础,而现有面向服务软件中异常处理逻辑复杂度高,导致难以为其构建支持可终止性分析的模型.本文基于着色Petri网构建了面向服务软件中异常处理逻辑模型(Exception Handling Logic Model for Termination Analysis,TA-EHLM),能为可终止性分析提供有效支持.为了建立该模型,提出了面向服务软件中异常处理的建模方法,给出了其形式化语义模型;根据该语义模型建模方法及模块组合思想,通过组合多个异常处理逻辑模块和正常业务逻辑模块,形成了TA-EHLM模型.并在此基础上,分析和检测了异常处理可终止性,结果说明了该模型的有效性.
-
-
JIANG Cao-Qing;
蒋曹清;
YING Shi;
应时;
WEN Jing;
文静;
JIA Xiang-Yang;
贾向阳;
王一兵
- 《2012年第三届中国计算机学会服务计算学术会议》
| 2012年
-
摘要:
异常处理的可终止性是确保其正确性的重要基础,而现有面向服务软件中异常处理逻辑复杂度高,导致难以为其构建支持可终止性分析的模型.本文基于着色Petri网构建了面向服务软件中异常处理逻辑模型(Exception Handling Logic Model for Termination Analysis,TA-EHLM),能为可终止性分析提供有效支持.为了建立该模型,提出了面向服务软件中异常处理的建模方法,给出了其形式化语义模型;根据该语义模型建模方法及模块组合思想,通过组合多个异常处理逻辑模块和正常业务逻辑模块,形成了TA-EHLM模型.并在此基础上,分析和检测了异常处理可终止性,结果说明了该模型的有效性.
-
-
JIANG Cao-Qing;
蒋曹清;
YING Shi;
应时;
WEN Jing;
文静;
JIA Xiang-Yang;
贾向阳;
王一兵
- 《2012年第三届中国计算机学会服务计算学术会议》
| 2012年
-
摘要:
异常处理的可终止性是确保其正确性的重要基础,而现有面向服务软件中异常处理逻辑复杂度高,导致难以为其构建支持可终止性分析的模型.本文基于着色Petri网构建了面向服务软件中异常处理逻辑模型(Exception Handling Logic Model for Termination Analysis,TA-EHLM),能为可终止性分析提供有效支持.为了建立该模型,提出了面向服务软件中异常处理的建模方法,给出了其形式化语义模型;根据该语义模型建模方法及模块组合思想,通过组合多个异常处理逻辑模块和正常业务逻辑模块,形成了TA-EHLM模型.并在此基础上,分析和检测了异常处理可终止性,结果说明了该模型的有效性.
-
-
-
-
-
-
-
-
- 上海大学
- 公开公告日期:2022-09-20
-
摘要:
本发明公开了一种基于特征模型和特征形式化规格说明的产品派生方法,首先根据用户需求从特征模型中选择派生特定产品的特征,确定特征融合顺序。然后融合特征形式化规格说明的声明部分,同时利用功能场景表示每个特征的行为,生成功能场景路径。最后按照特征融合顺序,以特征两两融合的方式,对特征的功能场景路径进行匹配,将每对特征形式化规格说明进行融合,直到得出完整产品的形式化规格说明。通过结合结构化面向对象的形式化语言(Structured Object‑Oriented Formal Language,SOFL)描述每个特征的具体行为,以及结合特征模型生成特征融合序列,以特征对形式进行特征形式化规格说明的行为保持融合,使派生得到的产品有详细描述,从而进一步提高派生产品的质量。
-
-
-