-
公开(公告)号:CN107133430A
公开(公告)日:2017-09-05
申请号:CN201710434652.X
申请日:2017-06-09
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G06F17/50
Abstract: 本发明公开了一种可信飞行控制系统协同开发的任务分配建模装置,属于控制软件的协同开发技术、形式化验证领域。所述装置包括:系统协同模块,用于明确协同开发系统在各阶段的协同分配任务特征及任务关系;任务分解模块,用于根据协同分配任务特征及任务关系对系统进行构件分解得到对应的各待分配任务;任务分配建模模块,用于根据各待分配任务间的任务关系建立任务分配模型;形式化模块,用于对各待分配任务进行形式化描述;模型检测模块,用于根据形式化描述对任务分配模型进行规范化约束验证;反馈模块,用于在模型检测模块验证未通过时,定位并反馈异常。本发明实现了系统协同开发中任务分配的有效建模,保证了系统安全且提高了开发效率。
-
公开(公告)号:CN106970791A
公开(公告)日:2017-07-21
申请号:CN201710138191.1
申请日:2017-03-09
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G06F9/44
Abstract: 本发明公开了一种线性时态逻辑规范的通用并行挖掘系统,该系统包括:预处理模块、规范实例生成模块、规范实例验证模块、结果筛选模块。其中,预处理模块实现对日志文件进行分割处理,获取日志中出现的事件集合,并收集这些事件在日志中的出现位置信息;规范实例生成模块,利用输入的规范模板,结合日志中的事件集合,生成具体的线性时态逻辑规范实例。规范实例检验模块,负责利用预处理后的事件位置信息,计算规范实例在日志中的支持度、置信度;结果筛选模块,负责对挖掘的结果集合进行筛选,去除支持度、置信度不符合挖掘要求的规范实例。该挖掘系统充分利用了多线程技术进行并行计算,能够高效地挖掘任意类型的线性时态逻辑规范。
-
公开(公告)号:CN107133430B
公开(公告)日:2019-11-26
申请号:CN201710434652.X
申请日:2017-06-09
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G06F17/50
Abstract: 本发明公开了一种可信飞行控制系统协同开发的任务分配建模装置,属于控制软件的协同开发技术、形式化验证领域。所述装置包括:系统协同模块,用于明确协同开发系统在各阶段的协同分配任务特征及任务关系;任务分解模块,用于根据协同分配任务特征及任务关系对系统进行构件分解得到对应的各待分配任务;任务分配建模模块,用于根据各待分配任务间的任务关系建立任务分配模型;形式化模块,用于对各待分配任务进行形式化描述;模型检测模块,用于根据形式化描述对任务分配模型进行规范化约束验证;反馈模块,用于在模型检测模块验证未通过时,定位并反馈异常。本发明实现了系统协同开发中任务分配的有效建模,保证了系统安全且提高了开发效率。
-
公开(公告)号:CN107256308B
公开(公告)日:2019-10-08
申请号:CN201710433623.1
申请日:2017-06-09
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G06F17/50
Abstract: 本发明公开了一种基于协同开发系统的构件交互关系建模系统,属于控制软件的协同开发技术、形式化验证领域。所述系统包括:获取模块,用于获取构件关系描述模型;提取模块,用于提取构件关系描述模型中的构件依赖关系;分解模块,用于根据构件依赖关系分解构件关系描述模型得到子模型;重组模块,用于将子模型与构件关系描述模型中含有的构件重组得到重组模型;规范化模块,用于对重组模型进行规范化描述;验证模块,用于根据规规范化描述验证重组模型中的构件依赖关系;输入模块,用于当验证模块验证成功时,将重组模型作为构件交互关系模型并输出;获取模块,还用于当验证模块验证失败时,获取构件关系描述模型。
-
公开(公告)号:CN109143952A
公开(公告)日:2019-01-04
申请号:CN201810609281.9
申请日:2018-06-13
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G05B19/05
Abstract: 本发明提供一种可编程逻辑控制器编程语言转换系统,包括:抽象语法树转换模块、梯形图转换模块、功能块图转换模块、顺序功能表图转换模块、结构化文本转换模块、指令表转换模块、ICIL中间结构转换模块。本发明提出的可编程逻辑控制器编程语言转换系统能够实现IEC 61131‑3语言的统一转换,在不同厂商的PLC产品上进行开发和移植过程中,不必分别针对每种PLC语言编写相应的移植代码,且有利于后续深入开展基于该中间语言的形式化建模、分析及验证工作。
-
公开(公告)号:CN109032056A
公开(公告)日:2018-12-18
申请号:CN201810609274.9
申请日:2018-06-13
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G05B19/05
Abstract: 本发明提供一种可编程逻辑控制器编程语言转换方法,包括:抽象语法树转换步骤、梯形图转换步骤、功能块图转换步骤、顺序功能表图转换步骤、结构化文本转换步骤、指令表转换步骤、ICIL中间结构转换步骤。本发明提出的可编程逻辑控制器编程语言转换方法能够实现IEC 61131‑3语言的统一转换,在不同厂商的PLC产品上进行开发和移植过程中,不必分别针对每种PLC语言编写相应的移植代码,且有利于后续深入开展基于该中间语言的形式化建模、分析及验证工作。
-
公开(公告)号:CN108984163A
公开(公告)日:2018-12-11
申请号:CN201810772287.8
申请日:2018-07-13
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
Abstract: 一种基于IMCL模型的异构式多平台代码生成方法,包括,采用IMCL语言,对目标系统的功能进行刻画,获得目标系统的功能模型;采用形式化方法,对所述功能模型进行分解,获得对应所述目标系统中的一个或多个平台的一个或多个平台模型;将所述一个或多个平台模型映射到对应的平台,从而对所述平台模型进行细节补充;在抽象语法树的基础上,根据所述一个或多个平台的特点,设计对应的转换规则,从而将所述一个或多个平台模型转化为对应的平台代码。本发明解决了现有技术难以同时对多平台代码进行生成的问题,将功能模型分解用以目标平台代码的自动生成,并通过程序切片方法以及基于形式化系统依赖图的分解方法保证了功能和功能间的约束关系的不变性。
-
公开(公告)号:CN107423104A
公开(公告)日:2017-12-01
申请号:CN201710434653.4
申请日:2017-06-09
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
CPC classification number: G06F8/447 , G06F9/45558 , G06F2009/4557
Abstract: 本发明公开了一种基于虚拟机的程序运行系统,主要包括:使用开发工具将IEC61131-3程序导出为XML格式文件,再使用程序翻译器将XML格式文件翻译成高级语言程序,将可运行高级程序的虚拟机部署到多平台设备上,最后使用高级语言编译器将高级语言程序编译为可执行文件,然后部署到相应普通计算设备上。通过本发明可以使得在普通计算设备上运行IEC61131-3程序,进而可以代替传统的PLC,克服了传统PLC的价格比较高、通用性差、移植困难、缺乏开放的体系、需要受制于PLC厂商等缺点,同时一般计算设备的强大计算能力和优秀的网络环境使得IEC61131-3程序具有更高的稳定性和实时性。
-
公开(公告)号:CN107256181A
公开(公告)日:2017-10-17
申请号:CN201710434096.6
申请日:2017-06-09
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G06F9/54
CPC classification number: G06F9/541
Abstract: 本发明公开了一种接入多类型协同件的服务总线平台,涉及计算机技术领域。所述平台包括:多类型协同件,用于分别将各自的消息发送给对应的各总线适配器;多类型总线适配器,与多类型协同件对应,用于将对应的协同件发送来的消息转换为服务总线可接受格式的消息请求,并发送给服务总线;服务总线,用于整合来自多类型总线适配器的消息请求得到对应的响应数据,并通过多类型总线适配器返回响应数据给对应的协同件。本发明中,通过多类型总线适配器将对应的多类型协同件接入服务总线,形成智能化的服务总线平台,实现了协同开发过程中多源异构协同件的通信协作。
-
公开(公告)号:CN106980576A
公开(公告)日:2017-07-25
申请号:CN201710322906.9
申请日:2017-05-09
Applicant: 华东师范大学 , 上海丰蕾信息科技有限公司
IPC: G06F11/36
Abstract: 本发明公开了一种基于运行时验证技术的嵌入式系统软件调试系统,所述系统包括:I/O仿真模块、需求规范检查单元、调试功能模块、执行控制模块。其中需求规范检查单元包括规范解析模块、分析模块、验证模块和决策模块;I/O仿真模块用于调试程序的数据的输入和输出,连接开发环境和单片机。执行控制模块用于控制调试系统的进程和运行,对调试系统进行状态设置。需求规范检查单元用于运行时验证程序是否满足时序停止条件。调试功能模块用于触发之后,对暂停的程序进行调试。本发明基于运行时验证,对满足一定的时序条件的程序进行触发调试,使得程序更加规范严谨,能够提高工作效率。
-
-
-
-
-
-
-
-
-