基于Event-B与ADT的TACS形式化开发方法与验证

为克服Event-B方法在开发全新一代列车自主运行控制系统(Train Autonomous Circumambulate System,TACS)中所出现的建模复杂性问题,提出将抽象数据类型(Abstract Data Types,ADT)实例化与Event-B相结合的方法,对TACS进行形式化开发和验证。首先,根据TACS的需求以及案例研究等相关内容,提取TACS的功能需求和安全需求,并将功能需求和安全需求以非形式化的语言进行描述;然后,根据TACS的功能需求和安全需求进行模型精化层次的设计,避免因在抽象模型中建模复杂的需求而导致证明困难;最后,在模型中使用形式化语言Event-B对TACS的功能需求和安全需求进行建模并验证其正确性,且在建模过程中,利用ADT的抽象概念将轨道网络、轨道区域以及移动授权(Movement Authority,MA)等复杂系统组件在初始模型中指定组件的必要属性,且在后续系统建模过程必要的精化阶段引入组件的具体定义,以降低系统开发和证明的复杂度。结果表明:提出的方法有助于在早期开发阶段减少TACS中复杂的细节部分,使得证明义务成功率为100%,自动证明成功率占比83%,手动证明成功率仅占比仅17%,在简化证明义务的同时有效提高了自动化证明的占比。

基于Event-B的可靠智能合约自动生成方法

智能合约是一种以代码的方式执行合同条款的可计算交易协议,其应用场景与规模日益增长,承载着多达数十亿美元的各类资产。由于其代码缺陷可能会造成严重的经济损失,因此智能合约的可信开发成为技术关键。为此,提出了一种基于集合论语言Event-B的智能合约可信验证与自动生成方法。Event-B方法是一种基于精化的形式化方法,可用于规约、设计和验证软件系统。通过对智能合约的模型验证和可执行代码的自动生成技术,研发了自动转换工具EB2S,打通了形式化模型和智能合约编程语言的语义鸿沟和技术壁垒。最后,选取典型的在线支付智能合约场景,应用基于Event-B的智能合约模型自动生成合约代码,验证了EB2S转换工具的有效性。

一种基于Event-B语言的时间触发系统建模方法

安全关键信息物理系统的时间属性建模和验证至关重要。Event-B模型验证避免了基于状态遍历模型检查方法的状态空间爆炸问题,验证时耗少,适用于高并发系统。然而,常规的Event-B方法缺乏时间语义表达结构,特别是缺乏对可提高系统可预测性的时间触发属性的支持。首先,介绍支持时间触发系统的抽象建模框架TTEB,从系统行为和实现2个抽象层次对时间属性进行建模和精化。然后,通过有序事件链组成的时间触发转移描述行为层时间触发属性;通过全局时钟到分布式本地时钟的精化和分解实现行为模型到实现模型的转化;运用时间触发转移建模分布式时钟周期同步。最后,基于从车跟车系统建模与验证说明方法的可用性和有效性。

UML到Event-B的系统化转换方法

在面向对象的软件开发中,UML已经成为事实上的建模标准。然而,UML虽然直观容易理解和应用,却存在着不精确的语义,而且UML是一种半形式化的建模语言,无法进行形式化的验证。Event-B是一种基于大量数学谓词逻辑的形式化方法,虽然精确却难以理解和应用。因此,如何结合UML图和Event-B方法的优点是研究的重点,以往的方法都是基于UML零散图到Event-B的转换,缺乏系统的转换方法。系统性的转换方法可以实现UML中的元素与Event-B中的元素相对应统一。一般的软件系统是中型系统,中型系统采用用例图、类图、状态图和顺序图这四种图就可以很好地表达清楚,有了上述的四种图,软件生命周期的需求获取、分析、设计、详细设计就可以完全表达清楚。文章中分别给出了这四种图到Event-B的转换方法,并将该系统的转换方法应用到对安全性和可靠性要求较高的电梯控制系统中。基于该实例的研究,验证了UML到Event-B系统性转换方法的可行性和有效性。UML到Event-B的系统转换方法不仅有利于UML的精确化和软件从业人员的使用,而且增强了形式化方法的可理解性,有利于形式化方法的推广和应用。

基于Event-B方法的多应用智能卡的建模与开发

Event-B是一种基于集合论和谓词逻辑的形式化系统语言,能够采用精化策略为系统建立逐渐精化的模型。提出了如何将Event-B应用到实际工业领域的方法,包括重写需求、建立抽象模型及逐层精化三个步骤。首先从环境、功能、性质三个主要方面重写需求,明确精化策略;然后利用形式化方法建立抽象模型并验证该模型;最后,在正确的抽象模型上按照精化策略添加需求、逐层精化,并对每层模型进行验证,基于满足需求的最后一层模型,可进一步利用工具完成代码自动生成。该方法学采用精化理论,以逐层递增的方式明确被开发系统的需求及性质,并进行形式化建模与验证,确保了模型的正确性。为了说明该方法学的可行性,以真正工业界的多应用智能卡为实例,基于Event-B方法及其工具平台Rodin给出了该方法在实际建模及验证过程中的应用。

基于改进Event-B建模的高速列车追踪运行仿真研究

针对铁路移动闭塞系统中高速列车间隔动态实时变化的特征,结合Agent理论对Event-B方法中Machine动态属性进行改进,提出一种基于Event-B建模方法的高速列车追踪运行模型。给出高速列车追踪运行形式化控制策略,研究运行过程中速度变化关系、不同发车间隔时间对高速铁路运营的影响,得到相应的定量与定性分析。仿真结果表明,该模型能够准确描述高速列车追踪运行机理,有助于列车间隔动态控制,具有较强的适用性。

SPARDL模型的Event-B解释

针对由周期行为和模式转换机制组成的实时系统提出的SPARDL需求建模语言,详细阐明了其对应的SPARDL模型的Event-B解释。通过Event-B来解释SPARDL的语义,同时提出一种基于SPARDL模型特征的精化框架用于Event-B模型的开发。最后,通过案例研究的分析展示用Event-B对SPARDL模型建模和验证的方法的有效性。

基于Event-B方法的安全协议设计、建模与验证

随着软件精化验证方法以及Isabella/HOL、VCC等验证工具不断取得进展,研究者们开始采用精化方法和验证工具设计、建模安全协议和验证安全协议源程序的正确性.在介绍Event-B方法和验证工具Isabella/HOL、VCC的基础上,综述了基于Event-B方法的安全协议形式化设计、建模与源程序验证的典型研究工作,主要包括从需求规范到消息传递形式协议的安全协议精化设计、基于TPM(trusted platform module)的安全协议应用的精化建模以及从消息传递形式协议到代码的源程序精化验证.

基于Event-B的形式化建模关键技术研究

软件系统的规模和复杂程度不断提高而传统的需求分析方法难以确保软件的正确性和一致性,为软件系统的质量埋下了隐患。软件工程的实践表明,在开发过程中,错误发现得越早,修复得越早,付出的代价越小。为了确保软件的质量,可在软件开发的早期需求分析阶段,采用Event-B形式化方法描述软件的需求,并验证模型的正确性。以文件系统建模为例,该文讨论了如何利用Event-B方法,采用逐步精化的方式建立并验证模型,确保软件的正确性。

基于Event-B的一种联锁逻辑的形式化建模研究

铁路车站信号联锁逻辑的形式化描述无论对计算机联锁软件的研发,还是对联锁软件的第三方测试都是非常重要的。基于Event-B方法,利用自动机模型和形式化语言对车站的一种信号联锁逻辑进行建模研究,并通过逐步精化的方法扩展联锁功能,依赖不变式技术形式化地保证了该模型的安全性。所建模型通过Rodin平台的验证,结果表明它们是安全的。

基于EVENT-B的飞机起落架控制系统形式化建模

飞机起落架控制系统作为飞机的一个极其重要的部分,在飞机着陆、滑跑、起飞过程中起着非常重要的作用,该部分系统性能的好坏将直接影响整个飞机的安全性。飞机起落架系统作为一个极其复杂的系统,如果使用传统的建模语言对其进行建模,可能会使整个建模过程变得特别复杂,所以这里选择形式化语言Event-B和可视化插件IUML-B对其建模,这对飞机起落架控制系统的开发与研究有着重要的意义。

基于Event-B形式化分析UML模型一致性

软件工程实践中广泛采用UML作为建模语言,UML模型在演进过程中会引入UML模型一致性问题.采用Event-B形式化技术可以协助分析UML模型的一致性,提出UML模型向Event-B模型转换的方法和规范性要求,设计具体的转换算法,证明这些算法的规范性以及采用这些算法转换得到的Event-B模型和原UML模型的等价性.文中提出了基于EventB形式化分析UML模型一致性的方法,并通过具体的案例说明了方法的具体执行过程.结果证明:基于Event-B形式化分析UML模型一致性的方法是有效的,可帮助改进UML模型质量.

基于Event-B的中断管理需求和设计形式化建模与验证方法

随着软件复杂度的迅速增长,传统的基于测试的方法逐渐难以满足航天器操作系统的可靠性和安全性需求,形式化方法逐渐成为航天器操作系统安全可靠性的有效保障.基于Rodin平台,采用Event-B形式化语言,通过需求和设计重写、制定精化策略并逐步精化的方法,对航天嵌入式操作系统SpaceOS2的中断管理模块建立了需求层和设计层形式化模型,将模型检验和定理证明相结合,验证模型的正确性并且满足安全性质.

基于Event-B的计算机联锁安全规范描述与验证

本文结合具体的站场实例,基于Event-B方法对信号开放、道岔控制、进路解锁等联锁系统关键安全规范进行了形式化模型描述和验证分析,给出了严格的分析结果。工作表明,铁路信号联锁系统是具有复杂时序逻辑的控制系统,Event-B方法适合于该类系统的描述与验证。通过形式化的联锁安全规范描述与验证,可以在系统开发的早期及时发现设计错误或漏洞,有助于提高计算机联锁系统的软件开发质量。

基于Event-B的联锁进路控制建模验证方法研究

计算机联锁系统具有典型的安全苛求特性。传统的联锁软件开发方法难以完整准确地定义需求,单纯依靠测试也无法发现软件中的所有错误,使软件在功能完整性和安全性方面难以得到保证。本文利用形式化Event-B方法和相关工具对联锁系统的核心功能—进路控制的相关功能需求和安全需求进行了建模、精化和验证,对开发高安全苛求和高可靠性的联锁软件提供了新的方法借鉴。

基于Event-B的动态车载导航系统架构设计

传统的软件架构设计一般采用非形式化的方法,通过各类图表从不同角度对系统进行描述,这种架构设计方式依赖设计者的经验知识,无法保证设计质量。本文将形式化建模引入架构设计,通过严格的形式化定义描述系统运行过程及需求约束,在保证模型正确的基础上导出架构设计,从而保证架构设计质量。

基于Event-B的列车车载控制器系统的形式化建模

介绍了列车车载控制器系统(Vehicle On-borad controller system)的系统结构和功能,采用Event-B建模理论对VOBC的系统结构与功能模式做了建模所必要的功能(FUN)列表定义与环境规约(EV)分类描述,给出了基于Event-B方法的VOBC执行指令的建模流程并指出了模型的分层提精步骤,对最终建立好模型进行了验证。

基于Event-B对存在网络攻击的安全协议的改进研究

设计对指定类型的网络攻击具有防御能力的安全协议,通常是一项重要且具有挑战性的任务。即使知道安全协议容易受到某种攻击,对其进行合理的改进也并不容易。本研究提出了一个基于Event-B方法的通用框架,用来指导安全协议的修改,并验证改进后的协议可以防御已知的网络攻击。首先用初始模型对攻击场景高度抽象,通过对抽象模型的精化,得到反映真实攻击过程的具体模型。然后将描述协议行为的事件从模型中分离出来,单独对其进行精化改进,如果改进后的协议事件重组的模型与具体模型不存在精化关系,则改进的合理性可以得到验证。最后通过NSPK协议被攻击的案例展示了本研究所提出方法的可用性。该框架可用于开发协议,以避免由逻辑漏洞引起的攻击,并验证协议补丁的正确性。

矿井机车运输信号系统的Event-B建模与验证研究

人工编制联锁表难以保证联锁表的准确性,而且单纯依靠人工检查联锁表中每个表项的正确性也是一项非常繁琐的工作。文章针对目前存在的问题,利用形式化Event-B方法对机车运输信号平面布置图、进路联锁表和机车车辆运输信号设计规范进行建模,模型生成的证明义务通过与否验证了进路联锁表建立过程是否符合平面布置图和设计规范的要求,利用该种思路解决了人工检查联锁表存在的效率低和不确定性等问题。

基于Event-B的双机热备平台测试序列自动生成方法

为了确保双机热备平台满足相应的功能需求,需要对其进行功能测试。采用基于模型的测试方法,可以有效地避免人工手动生成测试中存在的不足,提高测试效率。利用Event-B方法对双机热备平台进行形式化建模,通过证明验证模型的正确性,并进一步利用L^1算法生成基于模型、满足平台测试需求的测试序列集,对于确保测试过程的完备性、提高测试效率有一定意义。