公开(公告)号：CN116521347A

公开(公告)日：2023-08-01

申请号：CN202310582145.6

申请日：2023-05-23

Applicant: 电子科技大学

Inventor： 李启明 ,  房文宇 ,  杨霞 ,  孙海泳

IPC: G06F9/48

Abstract: 本发明公开了一种嵌入式实时操作系统的调度算法优化方法，在嵌入式实时系统μC/OS‑II中支持两级优先级实时调度。扩展后的优先级机制，一级优先级由用户决定，允许用户直接为多个功能或重要性一致的任务分配相同的优先级；二级优先级根据用户指定的优先级策略由系统自动分配，同一优先级下的任务可以按照二级优先级进行调度。扩展后每个任务的优先级仍然是唯一的，其形式为prio1/prio2。在使用优先级位图算法管理一级优先级的基础上，本发明扩展了OSRdyTbl_2用于管理二级优先级。本发明涉及的调度算法优化改进分为三个阶段：任务就绪、任务查找和任务结束。本发明大幅增加了嵌入式实时系统的优先级数量和任务并发数，同时保持较低的系统开销和响应时间。

公开(公告)号：CN117931193A

公开(公告)日：2024-04-26

申请号：CN202311471285.2

申请日：2023-11-07

Applicant: 电子科技大学

Inventor： 张博林 ,  杨霞 ,  房文宇 ,  肖华君

IPC: G06F8/41 ,  G06F21/57

Abstract: 本发明一种自动形式化验证c语言高层属性的系统及方法，将将代码与高层属性导入生成抽象语法树，中间语言生成器将其进行关键提取与遍历，然后生成程序流图导入到属性与代码分析器，对于高层属性文档描述的高层属性进行提取，对函数进行变量提取，生成变量的依赖表，将函数输出到函数属性路径生成器，生成相应的逻辑公式，再将目标属性生成逻辑公式，再将其相关性进行合并，给符号求解器进行求解然后进行计算，如果都能计算成功，这说明这个属性在代码里被满足，如果有违反了属性则存在误报的可能将结果输出到抽象验证器中生成对应的抽象谓词域，通过不动点迭代生成抽象状态机，最后得到抽象状态图后可以验证目标属性通过任意可达路径是否正确。