CAJ | 학술논문

分布式实时系统是广泛应用在众多关键领域的一类复杂实时系统.为保证其上运行任务的实时性,传统基于最坏响应时间的调度分析方法往往包含了实际系统运行过程中无法达到的最坏情况,因此在这些情况下的分析结果过于悲观.基于自动机理论的模型检测方法的好处在于能够穷尽地搜索整个系统状态空间,得到精确的分析结果.为了利用形式化方法的优势来精确分析分布式系统上任务的调度性,建立了分布式系统上的任务形式化模型,提出了行为自动机和环境自动机以分别描述任务的执行语义及其外部到达关系,把任务的调度性分析转换为对自动机网络位置的可达性进行分析,证明了在某些调度策略下的调度性的可判定性,并给出了满足调度可判定性调度策略的条件和范围.基于上述结论,实现了一个支持分布式系统任务实时调度分析工具SCT(schedulability checking tool),并与其他工具进行了分析精确度和性能的比较.比较结果显示,SCT可以提供最为精确的分析结果,但同时也具有最长的分析时间.
분포식실시계통시엄범응용재음다관건영역적일류복잡실시계통.위보증기상운행임무적실시성,전통기우최배향응시간적조도분석방법왕왕포함료실제계통운행과정중무법체도적최배정황,인차재저사정황하적분석결과과우비관.기우자동궤이론적모형검측방법적호처재우능구궁진지수색정개계통상태공간,득도정학적분석결과.위료이용형식화방법적우세래정학분석분포식계통상임무적조도성,건립료분포식계통상적임무형식화모형,제출료행위자동궤화배경자동궤이분별묘술임무적집행어의급기외부도체관계,파임무적조도성분석전환위대자동궤망락위치적가체성진행분석,증명료재모사조도책략하적조도성적가판정성,병급출료만족조도가판정성조도책략적조건화범위.기우상술결론,실현료일개지지분포식계통임무실시조도분석공구SCT(schedulability checking tool),병여기타공구진행료분석정학도화성능적비교.비교결과현시,SCT가이제공최위정학적분석결과,단동시야구유최장적분석시간.