摘要:已有的基于点区间优先级时间Petri网分析实时嵌入式多核系统的工作, 存在以下不足: (1)点区间优先级时间Petri网只考虑每个任务的执行时间是一个固定值的情况, 而更多的实际应用中每个任务的执行时间是在一个区间范围内, 因此不能模拟这些应用; (2)没有实现从任务依赖图到点区间优先级时间Petri网的自动转化, 不便于工程设计人员使用; (3)没有考虑任务间互斥访问共享变量的情况. 为此, 定义了优先级时间Petri网(Pri-TPN)以弥补第1个不足; 定义带有资源分配与优先级的任务依赖图(TDG-RAP)以弥补第3个不足; 给出从TDG-RAP到Pri-TPN的转化规则与算法以弥补第2个不足, 以及基于Pri-TPN分析任务最坏执行时间与系统死锁的算法; 开发工具软件, 方便工程设计人员使用.

摘要:工作流可满足性是业务安全规划的基本问题, 正在面临高资源配比(资源数n显著大于步骤数k)造成的性能挑战. 在资源独立约束下, 其最高效求解途径是模式空间上的增量回溯法IPB. 为克服结点真实性验证的性能瓶颈, 它增量计算模式k指派(二部)图及其(左完备)匹配, 分别需要O(kn)和O(k2)时间. 利用父子模式的原子差异增量计算完全指派图, 只需O(n)时间, 特别是其实际性能, 将随模式块规模增长迅速提高. 但该图的O(kn)规模导致了同样的增量匹配时间. 进而引入完备k核心匹配概念, 证明其存在性等价于左完备匹配, 且其增量计算时间为O(k2). 由此, 建立了时间复杂度更低的最小增量模式回溯法. 在含互斥和两种全局值势约束而授权比例约为1/4的扩展公开实例集上进行实验, 结果表明: 当n/k=10(及n/k=100), 而k变化时, 该方法较IPB有平均超过2(及5)倍、最低1.5(及2.9)倍的性能优势; 当k=18(及k=36), 而n/k=2~4096(及n/k=2~2048)时, 该方法有平均超过2.6(及3.6)倍优势; 而较2021年Minizinc挑战赛的冠军求解器Google OR-Tools CP-SAT, 该方法最低有超过3倍优势.

摘要:

摘要:时间Petri网为实时系统提供了一种形式化的建模方法,时间计算树逻辑(TCTL)为描述实时系统与时间相关的设计需求提供了一种逻辑化的表达方式,因此,基于时间Petri网的TCTL模型检测广泛应用于实时系统的正确性验证.然而对于一些涉及优先级的实时系统,例如多核多任务实时系统,这里不仅需要考虑任务之间的时间约束,还要考虑任务执行的优先级以及引入优先级带来的抢占式调度问题,致使相应的建模和分析变得更加困难.为此,提出了点区间优先级时间Petri网,通过在时间Petri网上定义变迁发生的优先级以及变迁的可挂起性,从而可以模拟实时系统的抢占式调度机制.首先,高优先级的任务抢占低优先级的任务所占用的资源,导致后者被中断;然后,前者执行完毕后释放资源;最后,后者再次获得资源,从中断的地方恢复.通过点区间优先级时间Petri网来模拟多核多任务实时系统,使用TCTL来描述它们的设计需求,设计了相应的模型检测算法,开发了相应的模型检测器以验证它们的正确性.通过一个实例,来说明该模型和方法的有效性.