摘要：为满足网络化控制系统的综合性能要求,实现其设计过程的形式化和规范化,针对其设计过程进行了形式化建模。给出了网络化控制系统中网络、控制、结构实体三个子模型的定义,分析了三者的构成要素以及相互之间的映射关系;进而提出了基于网络服务质量和控制性能质量的协同设计框架,并利用统一建模语言进行网络化控制系统的结构实体子模型设计,分析了网络化控制系统建模中类的概念和构造,针对类的属性和方法进行了扩展,归纳了建模过程的一般性步骤。最后以一台网络化三轴数控钻床的设计过程为例,实现并验证了所提出协同设计框架与形式化建模过程的可行性。

摘要：在参考多智体系统的基础上,根据大系统控制论的分解协调思想,提出一种软件人群体体系结构,并对其关键技术如本体库、知识库、任务库、通信协议、角色模型、交互模型等进行了描述.描述了对该系统从分析到设计的整个构建过程,并采用π演算形式化方法对整个系统的信息流和控制流,以及任务之间的4种协作方式进行了建模.对于不同的应用领域,通过定义相应领域的本体库和所需的角色以及任务分解,即可快速构建相应的应用系统,为分布式系统提供了一种解决方案.

摘要：为了保证一种非常经典的适用大规模存储地NAND闪存上的DFTL算法的正确性,对DFTL算法采用了形式化建模的方法来建立一个高可信的形式化模型.根据DFTL算法提出者的设计,我们以此为依据,对DFTL算法的基本数据结构,读写操作和垃圾回收操作以及基本性质进行了形式化的建模和验证,并对文中提出的垃圾回收算法进行了适当的修改和优化,以证明垃圾回收算法的正确性.最后我们针对DFTL算法,设计了一个验证框架,在这个验证框架和形式化的NAND闪存模型的基础上,对DFTL算法的的一些基本性质进行了验证.

摘要：为了提升新一代航空电子全双工交换以太网(AFDX)网络的传输速率和余度设计可靠性,在AFDX网络标准的基础上(ARINC 664 p7),建立千兆三余度AFDX网络的帧管理机制模型并进行了形式化建模,而且实现了AFDX网络标准中描述的SkewMax机制。使用UPPAAL形式化工具对千兆三余度AFDX网络帧管理机制进行形式化验证,验证帧管理机制的完整性检查及冗余管理功能的可用性。结果表明,千兆三余度AFDX网络帧传输过程中不存在死锁。此外,针对标准AFDX的冗余管理中一个帧的丢失可能会导致其冗余备份的丢失的现象,提出在接收端设置一个队列,记录那些比连续帧更晚到达的冗余备份的帧序号,从而减少不必要的丢帧,提高QoS和数据完整性。形式化验证的结果可以作为千兆AFDX网络标准制定和实际应用的参考。

摘要：传统遥感数据处理流程分散且独立,缺乏形式化语义模型,更没有通用的遥感数据处理流程自动形式化建模方法,难以进行有效分析和验证,不利于实现计算机对遥感数据处理流程的自动控制.针对以上问题,本文结合Petri网建模的相关研究成果,构建适合遥感数据处理流程的形式化描述模型RSDP_Net(Remote Sensing Data Processing Net),并研究其验证方法;设计一种基于自然语言的半结构化文档描述遥感数据处理流程,并开发由该文档向RSDP_Net的自动转化工具,从而达到实现自动构建遥感数据处理流程形式化模型的目的.最后,以遥感数据提取植被面积流程为例,使用该方法自动生成流程形式化模型.

摘要：温室环境测控系统由多个可并发执行的子系统共同协作来构造适宜的温室环境以确保作物有效生长.为提高温室环境测控系统设计的效率和可靠性,本文提出一个能为设计者提供指导性框架的融入容错技术的高可靠性温室环境测控系统架构.并且运用PVS形式化语言对系统架构进行了精确而无二义性的形式化建模,以及PVS证明工具对系统架构的容错特性进行了机械化证明,以确保系统架构能满足高可靠性需求.

摘要：通过剖析影响可生存性的本质特征,将服务请求与服务器、攻击者与服务器描述为不同的组件,使用PEPA语言精确描述系统各个状态间的逻辑关系和动态变化过程,从用户服务请求和攻击影响两个角度分别构建可生存性形式化模型,并比较两种建模角度的异同。理论分析和实验结果表明该模型能够正确地反映出可生存性的关键属性,并可在理论上指导可生存系统的设计和实现。

摘要：随着课堂教学从固化单一的教师传授,向强调小组协作参与的教学转变,如何面向以协作学习为基本特征的课堂实施形成性评价已成为教学评价改革亟需解决的问题。在智能技术支持下,形式化建模可以将复杂多变的课堂教学过程解构,形成数理模型;智能计算可以通过算法评估学生学习状态,并根据教学原则生成教学辅助信息。二者的结合可以促进人类智能与机器智能的有效融合,形成人机协同的课堂评价机制。面向课堂教学评价的形式化建模与智能计算通用架构,自下而上包含教与学行为的感知和存储、教与学行为评估模型的构建、教与学状态的智能计算和教学辅助信息的生成四个部分。前两部分着重对教育情境和问题的表征,是形式化建模的关键步骤;后两部分着重具体技术路线的实现,是智能计算的具体过程和功能体现。整个系统以教与学行为的感知和存储为基础,通过构建评估模型,确定模型的输出;然后引入智能算法对模型进行计算,达成对教与学状态的评估;最后根据相应教学原则,自动生成辅助教师进行课堂教学评价的信息。该通用架构以及人机协同教学、评价机制的进一步完善需要研究者携手教师进行"共同设计",协同教育学、计算机科学、心理学等多学科进行交叉研究。

摘要：语法和语义层次的组合并不足以保证仿真组件组合的完整性、有效性和实用性,在语用组合问题分析的基础上,提出了基于扩展有限状态自动机的仿真组件模型形式化描述,包含了仿真组件行为语义和仿真运行语境约束信息,并在此基础上设计了基于XML的仿真组件模型描述规范。最后,通过应用实例具体描述了面向语用组合的仿真组件模型组合过程。组合中考虑了模型发现、组合判定、仿真运行与仿真语境之间的关系,并且实现了面向语用的仿真系统自动化动态构建。

摘要：目前数据库形式化安全策略模型存在抽象层次较高、缺乏对数据库状态与约束的充分描述等问题,难以辅助用户发现商用数据库设计中的微小缺陷。提出了一种基于PVS语言的数据库形式化安全策略模型建模和分析方法,该方法较以往模型能够更加贴近实际数据库,应用范围更广,安全属性描述更加完整,描述的模型具有灵活的可扩展性,并且保证了建模与验证的效率。最后,将该方法应用于数据库管理系统Beyon DB的安全策略建模分析中,帮助发现了系统若干设计缺陷,证明了方法的有效性。