形式化建模
形式化建模的相关文献在2004年到2022年内共计154篇,主要集中在自动化技术、计算机技术、铁路运输、航空
等领域,其中期刊论文94篇、会议论文23篇、专利文献587846篇;相关期刊63种,包括西安交通大学学报、计算机工程、计算机工程与科学等;
相关会议22种,包括第十五届全国Petri 网理论与应用学术会议、第九届中国系统建模与仿真技术高层论坛、全国抗恶劣环境计算机第二十四届学术年会等;形式化建模的相关文献由371位作者贡献,包括王健、赵国生、李晓红等。
形式化建模—发文量
专利文献>
论文:587846篇
占比:99.98%
总计:587963篇
形式化建模
-研究学者
- 王健
- 赵国生
- 李晓红
- 熊焰
- 郭建
- 黄文超
- 乔磊
- 周庭梁
- 杨惠珍
- 杨桦
- 熊峰
- 郝莉莉
- 刘波
- 刘静
- 吴尽昭
- 唐涛
- 徐中伟
- 李钦
- 罗娟
- 赵永望
- 陈小红
- LI Hua
- 丁剑杰
- 侯红
- 冒苏敏
- 冯世玲
- 刘方
- 刘海龙
- 刘美玲
- 刘鸿瑾
- 吕继东
- 吴晓菲
- 周乐
- 喻钢
- 姚静晶
- 孙达志
- 孟昭逸
- 张佑生
- 张杰
- 张江
- 张福景
- 张程
- 张程伟
- 张立臣
- 张蕾
- 张锦坤
- 徐锐
- 方贤进
- 曲良东
- 曾国荪
-
-
孟开元;
王瑾;
彭寒;
曹庆年
-
-
摘要:
飞机起落架控制系统作为飞机的一个极其重要的部分,在飞机着陆、滑跑、起飞过程中起着非常重要的作用,该部分系统性能的好坏将直接影响整个飞机的安全性。飞机起落架系统作为一个极其复杂的系统,如果使用传统的建模语言对其进行建模,可能会使整个建模过程变得特别复杂,所以这里选择形式化语言Event-B和可视化插件IUML-B对其建模,这对飞机起落架控制系统的开发与研究有着重要的意义。
-
-
谢小赋;
曾梦岐;
庞飞
-
-
摘要:
计算机并发性程序形式化验证一直是软件安全领域的难题。软件并发性漏洞难以被发现,一旦发生问题,会造成不可估量的安全问题。形式化验证基于严格的数学推导基础,采用语言、语义、推理证明三位一体方法,构建形式逻辑系统,以确保被验证系统的安全性能。传统的形式化验证方法由于人工参与多、验证工作量大、验证效率低等不足,难以对计算机并发程序进行严谨高效的模型描述与验证。研究了一种可双向转换的并发性程序形式化验证方法,解决了人工抽象建模存在的工作量大且易出错的问题,并且保证了源码层与抽象层验证的一致性,大幅提升了形式化验证的效率。
-
-
刘美山
-
-
摘要:
本文首先了解航空电子系统的典型软件体系结构,在形式化建模视角下分别对航空电子系统进行静态建模和动态建模,提出了形式化的航空电子系统综合检测方法,同样从静态和动态两方面对航空电子系统进行全面检测研究。
-
-
朱国锋;
陈昊
-
-
摘要:
航空电子系统经过数十年的演进,正朝着更加开放、灵活、智能的方向发展,同时也不断面临新的问题和挑战,需要在功能复杂度不断提升的前提下实现资源的高效分配,保证系统的实时性与可靠性。通过分析机载嵌入式计算特点,基于模型的系统工程理论的同时结合形式化建模仿真方法,针对典型嵌入式计算平台场景中的组件开展基于模型的设计方法研究与应用。该方法能够清晰描述航电嵌入式计算的时间关键性特征,有效辅助设计和论证工作,降低研发周期、提升设计的可复用性。
-
-
张立山;
冯硕;
李亭亭
-
-
摘要:
随着课堂教学从固化单一的教师传授,向强调小组协作参与的教学转变,如何面向以协作学习为基本特征的课堂实施形成性评价已成为教学评价改革亟需解决的问题.在智能技术支持下,形式化建模可以将复杂多变的课堂教学过程解构,形成数理模型;智能计算可以通过算法评估学生学习状态,并根据教学原则生成教学辅助信息.二者的结合可以促进人类智能与机器智能的有效融合,形成人机协同的课堂评价机制.面向课堂教学评价的形式化建模与智能计算通用架构,自下而上包含教与学行为的感知和存储、教与学行为评估模型的构建、教与学状态的智能计算和教学辅助信息的生成四个部分.前两部分着重对教育情境和问题的表征,是形式化建模的关键步骤;后两部分着重具体技术路线的实现,是智能计算的具体过程和功能体现.整个系统以教与学行为的感知和存储为基础,通过构建评估模型,确定模型的输出;然后引入智能算法对模型进行计算,达成对教与学状态的评估;最后根据相应教学原则,自动生成辅助教师进行课堂教学评价的信息.该通用架构以及人机协同教学、评价机制的进一步完善需要研究者携手教师进行"共同设计",协同教育学、计算机科学、心理学等多学科进行交叉研究.
-
-
夏锐;
钱振江;
刘苇
-
-
摘要:
传统对称密钥加密协议的加密和解密速度较快,但用户无法进行身份认证,容易造成通信代理持有密钥过多导致管理困难的问题,而非对称密钥加密协议可实现用户的合法身份认证,但密钥复杂度高,使其在处理大容量消息时运行速度较慢.为解决上述问题,结合对称和非对称密钥加密方式,构建D protocol混合密钥加密协议.使用Isabelle/HOL定理证明辅助工具对D protocol协议建立通信代理和消息序列的形式化模型,采用形式化操作语义描述用户行为,通过归纳分析方式对通信协议消息交互过程涉及的相关定理展开验证,结果表明D protocol协议在提高通信效率的同时具有较高的安全性,并且可在一定程度上抵抗外部攻击和中间人攻击.
-
-
程宝;
张福景
-
-
摘要:
TCMS(Train Control and Management System)是列车运行控制、数据监测的中枢,文章分析磁浮列车TCMS的系统拓扑和功能需求,建立时间自动机模型,运用UPPAAL验证工具对TCMS的安全性和时效性进行验证。结果表明,时间自动机对于磁浮列车的TCMS建模和验证效果良好。
-
-
程宝;
张福景
-
-
摘要:
TCMS(Train Control and Management System)是列车运行控制、数据监测的中枢,文章分析磁浮列车TCMS的系统拓扑和功能需求,建立时间自动机模型,运用UPPAAL验证工具对TCMS的安全性和时效性进行验证.结果表明,时间自动机对于磁浮列车的TCMS建模和验证效果良好.
-
-
刘秉政;
高松;
曹凯;
王鹏伟;
徐艺
-
-
摘要:
由于传统车辆跟驰建模预测方法无法遍历车辆所有可能的系统输入与运行状态的不确定性,因而不足以从理论上保证对周边车辆安全跟驰行为预测的完整性与可信性.为此提出车辆安全跟驰模式预测的形式化建模方法.该方法利用随机可达集的遍历表现特征实现对周边车辆行为预测的不确定性表述,并通过马尔科夫链逼近可达集的方式表达系统行为状态变化的随机性,从而完成对周边车辆跟驰行为状态变化的精确概率预估.为了表达跟驰情形中车辆之间的行为关联影响以及提高在线计算效率,离线构建了关联车辆在状态及控制输入之间的安全关联矩阵,描述周边车辆的安全跟驰控制输入选择规律,并综合相关车辆的当前状态信息,达到对周边车辆安全跟驰行为的在线分析与预估.数值验证不仅表明提出的建模方法完备地表述了周边车辆所有的安全跟驰行为及过程,显著提高了预测的精确度,也论证了该方法对车辆跟驰控制策略建模分析与安全验证的有效性.
-
-
-
WANG Run;
汪润;
ZHAO Lei;
赵磊;
XIONG Qi;
熊琦
- 《第九届信息安全漏洞分析与风险评估大会(VARA2016)》
| 2016年
-
摘要:
监控与数据采集(SCADA)系统是一种主要的工业控制系统类型.DNP3是标准的SCADA协议,主要用于主控站和节点之间通信,DNP3-SA是DNP3协议中一种用于保证端到端通信安全的安全认证机制.本文利用有色Petri网对DNP3-SA协议进行形式化建模,文中提出的DNP3-SA有色Petri网模型可以测试和验证篡改等攻击场景.利用文中有色Petri网模型分析发现了DNP3-SA协议中的一个未知安全隐患,攻击者在没有共享密钥的条件下通过使用任意的变量可以重放认证命令,能够通过网络访问DNP3设备.
-
-
吴文娟;
马殿富;
赵永望;
赵宪琦
- 《全国抗恶劣环境计算机第二十四届学术年会》
| 2014年
-
摘要:
航空机载软件适航认证DO-178C的发布对机载软件提出了更高的安全性和可靠性需求,对机载软件建模及验证提出了重大挑战.为了达到机载软件高层需求目标,提出一种基于知识图的高层需求的形式化建模方法,此方法给出一种形式化语言描述知识图并协同构建知识图,然后通过因果模型表示高层需求,通过知识图对功能需求和非功能需求形式化建模.这提高了需求可追溯性,即有助于从高层需求追溯到系统需求来实现DO-178C提出的高层需求可追溯性目标.而且,我们提供建模工具让领域专家协同构建知识图并实现高层需求建模,我们也给出一些高层需求验证,这些对生成安全、可靠、高质量的机载软件系统意义重大.
-
-
王健;
赵国生
- 《第三届中国计算机网络与信息安全学术会议(CCNIS2010)》
| 2010年
-
摘要:
提出一种基于性能评估进程代数的网络可生存性形式化建模方法。通过剖析影响可生存性的本质特征,将服务请求与服务器、攻击者与服务器描述为不同的组件,使用PEPA语言精确描述系统各个状态问的逻辑关系和动态变化过程,从用户服务请求和攻击影响两个角度分别构建网络可生存性形式化模型,并比较两种建模角度的异同。理论分析和实验结果表明了本文所提方法的合理性和有效性,该模型能够正确地反映出可生存性的关键属性,并可在理论上指导可生存系统的设计和实现。
-
-
-
郝莉莉;
杨惠珍
- 《2010中国科协海峡两岸青年科学家学术活动月“仿真科学与技术”学术研讨会》
| 2010年
-
摘要:
联邦概念模型是整个联邦系统开发的依据,采用形式化的方法建立和验证联邦概念模型有助于提高模型的可重用性和可信度。分析了国内外形式化建模与验证方法研究的现状,提出了一种基于着色Petri 网的联邦概念模型形式化建模与验证方法,给出了用着色Petri 网建立与验证联邦概念模型的步骤,并以一制造系统为例,利用CPN Tools建立了系统的联邦概念模型,验证了所建模型的活性、家态和公平性。研究表明,着色Petri网能够为联邦概念模型的形式化建模和验证提供有效的支持。
-
-
LI Hua;
李华;
XING Yi;
邢熠;
ZHANG Yu-Rong;
张玉荣
- 《第十五届全国Petri 网理论与应用学术会议》
| 2015年
-
摘要:
CPN形式化建模适合为包含大量并发、通信、同步共享行为的软硬件系统建立形式模型,并完成系统功能和性能等方面的行为分析.在传统的CPN建模中,token的选取采用穷举法,生成的token数量较多,并且CPN模型生成的状态空间相当庞大,甚至状态空间爆炸等问题.针对上述问题,将符号执行与CPN建模相结合,并在CPN模型的执行过程中采用一种基于token选取的方法,进而得到CPN模型的状态可达图.通过对OpenStack云平台支持创建的单一平面网络进行CPN建模,针对传统方法和本文方法生成状态空间分析了规模的变化,验证了本文提出的方法的有效性.
-
-
杨楠;
张清辉;
宋崴;
赵鹏
- 《第九届中国系统建模与仿真技术高层论坛》
| 2014年
-
摘要:
本文对军事训练游戏剧情需求形式化建模进行了研究.针对军事领域专家与游戏设计与开发领域专家之间存在较大的知识壁垒,相互交流困难问题,提出了基于活动图的军事训练游戏剧情需求形式化建模描述方法.首先对军事训练游戏剧情活动图的语法及语义进行了定义,然后提出了基于活动图的军事训练游戏剧情需求建模描述方法,最后通过实例对本文提出的方法进行了应用.应用结果表明通过本文提出的方法对军事训练游戏剧情需求进行建模有效地实现了军事训练游戏剧情需求描述的形式化和规范化,有利于军事训练游戏设计与开发人员的理解,有助于游戏剧情需求提出人员与游戏设计开发人员之间的交流.
-
-
-
郭炜锋;
赵伟;
赵永望
- 《全国抗恶劣环境计算机第二十八届学术年会》
| 2018年
-
摘要:
形式化方法的系统设计、验证以及自动代码生成已经在单核系统上形成很多研究成果,但在多核并发系统上的研究仍面临许多科学问题.多核并发系统验证的难点在于验证者需要考虑多核并发系统中线程穿插执行造成的不确定性.本文基于Event-B形式化方法,提出了一种基于共享变量的组合推理方法解决多核并发系统验证中线程交互的不确定性问题.通过并发队列的验证实验,证明了该方法的有效性和正确性.未来的工作会将此方法形成具体的验证框架,进行ARINC653多核分区操作系统标准的验证.
-
-
郭炜锋;
赵伟;
赵永望
- 《全国抗恶劣环境计算机第二十八届学术年会》
| 2018年
-
摘要:
形式化方法的系统设计、验证以及自动代码生成已经在单核系统上形成很多研究成果,但在多核并发系统上的研究仍面临许多科学问题.多核并发系统验证的难点在于验证者需要考虑多核并发系统中线程穿插执行造成的不确定性.本文基于Event-B形式化方法,提出了一种基于共享变量的组合推理方法解决多核并发系统验证中线程交互的不确定性问题.通过并发队列的验证实验,证明了该方法的有效性和正确性.未来的工作会将此方法形成具体的验证框架,进行ARINC653多核分区操作系统标准的验证.