并发系统中基于优先级的调度分析

Analyzing Scheduling Based on Priority in Concurrent Systems

当前复杂的并发系统多采用模块化、逐步求精和信息隐藏等非形式化的原则来指导系统的开发,而这些指导原则抽象且无法保证分解系统的正确性。为此,对基于优先级控制的系统分解方法展开研究,提出一种系统分解的方法,并在理论上证明该分解方法的正确性。首先采用基于事件的行为模型对系统进行建模;接着定义调度、调度策略和调度策略正确性的概念;然后研究调度策略的分解方法,并证明了调度策略分解方法的正确性;最后根据该方法,开发出一种支持依赖模型建模和调度策略分解的原型工具,通过实例的演示,说明了使用该方法可以把系统分解成若干个子系统,从而设计出正确和有效的调度策略,以达到正确分解系统的目的。

Due to the complexity of the concurrent system,it is difficult for engineers to develop a complex system as a whole directly.They often apply informal principles,such as modular,stepwise refinement and information hiding,to guide system development.These guidelines are abstract and can't guarantee the correct decomposition of system.In this paper,we focused on the system decomposition method based on priority,proposed a method to decompose the system,and proved its correctness.First,we modeled system with an event-based behavioral model.Next,based on such a model,we formally defined the schedule,the scheduling policy and the correctness of a scheduling policy.After that,we proposed a method for decomposing schedule policy,and proved the method's correctness.Finally,according to the decentralized method,we developed a toolkit,which supports event-based behavioral model,for modeling system and decomposition of scheduling policy.An experiment demonstrates that these results may help engineers to design correct and efficient schedule policies in a system to realize decomposition.