资源受限的实时进程代数

理论计算机科学电子笔记162（2006）221-226www.elsevier.com/locate/entcs一类资源受限的实时进程代数Insup Leea，1 Anna Philippoub，2，Oleg Sokolskya，3a宾夕法尼亚大学计算机和信息科学系，南33街200号，关闭PA，USAb塞浦路斯大学计算机科学系，P.O. Box 20537，尼科西亚，塞浦路斯摘要通信共享资源代数（ACSR）是一个时间进程代数，它扩展了经典进程代数的资源概念。它认为，实时系统的定时行为不仅取决于由于进程同步的延迟，而且还取决于共享资源的可用性。因此，ACSR使用资源作为基本原语，并将实时系统表示为一种并发进程的集合，这些进程可以通过瞬时事件相互通信，并竞争共享资源的使用。 资源用于对物理设备进行建模，作为处理器、存储器模块、通信链路或任何其它容量有限的可重用资源。此外，它们还提供了一种方便的抽象机制，用于捕获系统行为的各个方面。由此产生的框架结合了进程代数和实时调度的领域，并可以促进推理系统的最后期限，进程交互和资源可用性是敏感的。本文介绍了ACSR及其扩展PACSR、P2ACSR和MCSR，它们考虑了概率故障、功耗和多容量资源。保留字：实时进程代数，资源建模，概率行为，功耗1引言系统行为的时序建模在进程代数形式主义中有着悠久的历史。在本文中，我们提倡使用资源的实时系统建模的一种手段，达到更简单，更忠实的模型。进程代数，如CCS [7]，CSP [4]和ACP [2]，已被开发用于描述和分析通信，并发执行系统。它们基于这样的前提：理解复杂性的两个最基本的概念这项研究得到了ARO DAAD 19 -01-1-0473、ARO W 911 NF-05-1-0182、NSF CCR- 0209024、NSF CNS-0509327和NSF CNS-0509143的部分支持。1 电子邮件地址：lee@cis.upenn.edu2 电子邮件地址：annap@cs.ucy.ac.cy3 电子邮件地址：sokolsky@cis.upenn.edu1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.085222I. Lee等人/理论计算机科学电子笔记162（2006）221动态系统是并发和通信[7]。Lee等人提出的共享资源通信代数（ACSR）是一种新的通信算法。[6]，是一个时间进程代数，可以看作是CCS的一个扩展。实时系统的定时行为不仅取决于进程同步引起的延迟，还取决于共享资源的可用性。大多数实时进程代数适当地捕获由于进程同步引起的延迟。然而，它们通过假设理想化的操作环境来抽象出资源特定的细节另一方面，用于实时系统的调度和资源分配算法ACSR代数提供了一个正式的框架，进程代数和实时调度的领域，因此，可以帮助我们推理对截止日期、进程交互和资源可用性敏感的系统。ACSR的计算模型是基于这样的观点，即实时系统由一组使用共享资源执行并彼此同步的通信进程ACSR中的实时概念是定量的和离散的，并且使用定时动作的概念来适应。执行一个定时动作需要访问一组资源，并花费一个时间单位。资源是连续可重用的，对它们的访问由优先级控制为了确保时间的一致进展，进程同步执行定时操作与CCS类似，事件的执行是即时的，从不消耗任何资源。通信的概念是通过执行补充事件使用事件建模的，然后将补充事件转换为内部事件。进程异步执行事件，除非两个进程通过匹配事件同步。优先级用于在可能同时发生多个事件时指导选择。本文将ACSR扩展为一类进程代数，GCSR [1]，稠密时间ACSR [3]，ACSR-VP[5]，PACSR [8]和P2ACSR [10]. GCSR允许ACSR工艺的可视化表示。ACSR-VP通过值传递功能扩展了ACSR，扩展了可以处理的调度问题的类别PACSR允许用概率对资源故障进行建模，而P2ACSR增加了功耗的概念.下面将非正式地介绍其中一些扩展2资源受限流程2.1计算模型我们区分两种类型的行动：消耗时间的行动和瞬间的行动定时动作可能需要访问系统资源，例如，CPU相比之下，即时操作提供了并发进程之间的同步机制。定时行动。一个系统有一组有限的可重复使用的资源，R。一个动作消耗一个“ 滴答 ”的时 间，并使 用一组 资源，每 个资源 都有一个 整数优 先级。例 如，action{（r，p）}表示使用某个资源I. Lee等人/理论计算机科学电子笔记162（2006）221223r∈ R在优先级p上运行。不消耗任何资源的操作“空闲”表示一个时间单位的空闲。事件瞬时动作或事件在ACSR中提供进程同步。事件由一对（a，p）表示，其中a是事件的标签，p是其优先级。标签表示通道上的输入和输出操作。与CCS中一样，当两个事件的输入和输出在同一频道同步2.2实时进程ACSR过程由以下语法描述，其中我们假设一组过程 具有一个 相关的 定义，即Cd=efP。P：：= 无|（a，n）.P|答：P|P + P| PP|P\F|[P] I|P\\I|一PΔt（P，P，P）|CACSR过程的步骤使用与两种类型的动作相对应的两个前缀运算符来构造进程（a，n）.P执行瞬时事件（a，n）并前进到P。进程A：P在第一个时间单元执行一个消耗资源的动作，然后继续前进到P。 过程P+Q表示非确定性选择和过程P_PQ描述了并发组合一的P和Q。 时间作用域构造PΔt（Q，R，S）限制过程P时间限制（T）。如果P在此限制内完成其执行，则异常a，在这种情况下，执行异常处理程序（Q）。如果不是，则将控制传递给超时进程（R）。在任何情况下，P都可以被中断过程（S）的步骤中断。ACSR的其他静态操作符允许我们隐藏某些资源的身份（P\\I），为给定进程保留资源的使用（[P]I），并通过限制某些事件（P\F）来强制进程之间的同步。进程的执行由定时标记转换系统（定时LTS）定义。一个定时LTS，M，定义为P，D，→，P0，其中P是一组ACSR过程，由P，Q，D是一组动作，→是一个标记α如果P−→Qifproces P可以在数据库中使用，事件或定时动作α，然后表现为Q。P0∈ P表示系统的初始状态。实时系统分析。在ACSR的形式主义，我们可以进行两种类型的实时调度分析：验证和可扩展性分析。验证表明，给定的规范正确地模拟了所需的实时调度规则，例如速率单调和最早截止日期优先。可调度性分析确定具有特定调度规则的实时系统是否错过其任何截止日期。实时系统的验证和可验证性分析可通过在代表所考虑系统的ACSR过程及其规范之间建立适当的等效性来进行。224I. Lee等人/理论计算机科学电子笔记162（2006）2212.3资源概率和操作PACSR（ProbabilityACSR）通过将每个资源与概率相关联来扩展ACSR。此概率捕获资源可能发生故障的速率。因此，定时操作现在可以解释资源故障。定时行动。 除了ACSR资源集合R之外，我们考虑集合对于每个r∈ R，r表示失败的资源r。行动ACSR中的构造，但现在可以包含正常和故障资源。如果r失败，则操作{（r，p）}不会发生。另一方面，动作{（r，q）}仅在资源r失败时发生。此表示法对于指定从故障中恢复非常有用。资源概率。在PACSR中，我们将每个资源与该资源可能发生故障的概率相关联。 我们用p（r）∈[0，1]表示资源r可用的概率，而p（r）= 1−p（r）是资源r失效的概率。资源消耗过程的这种概率行为反映在opera中PACSR的语义。例如，考虑进程{（cpu，1）}：NIL，其中p（cpu）= 2/ 3。然后，以2/ 3的概率，资源cpu可用，进程可以执行该步骤，而以1/ 3的概率，资源失败，进程死锁。概率过程。PACSR进程的语法与ACSR的语法相同。唯一的扩展涉及在时间上出现失败的资源行动因此，一方面可以将故障概率分配给现有ACSR规范的资源并对其进行概率分析，另一方面可以忽略故障概率并对PACSR规范进行非概率分析。PACSR的语义是通过两个转移关系定义的过程的概率和非确定性的可操作性。由此产生的过渡系统属于一类标记的并发马尔可夫链[11]。概率系统分析。我们定义了概率弱互模拟[9]，它允许我们比较PACSR过程的可观察行为，类似于ACSR的情况。此外，概率转移中的概率信息使我们能够对PACSR规格。特别是，我们可以计算到达给定状态或死锁状态的概率，或者我们可以对PACSR规范进行模型检查[8]。2.4功耗感知流程通常，除了可重用的资源之外，我们还需要对可消耗的资源（如电源）进行建模。PACSR的一个扩展称为P2ACSR，它允许我们通过指定访问资源时消耗的功率来推断功耗感知进程资源和电力消耗。为了推断分布式设置中的功率消耗，将资源集合R划分为不相交类的有限集合Ri。直观地说，每个Ri对应于不同的电源I. Lee等人/理论计算机科学电子笔记162（2006）221225其可以提供有限量的功率C1。 每个资源r ∈ Ri消耗来自Ri的一定量的功率。与PACSR一样，每个资源都有固定的故障概率。耗电的定时动作。定时动作被扩展为包括资源消耗的功率形式上，动作是形式为（r，p，c）的三元组的有限集合，其中r是资源，p是资源使用的优先级，c是功耗率。对动作的附加限制是任何资源类别的总功耗不超过该类别的限制。通过对PACSR的转移关系的扩展，将其语义再次表示为标号并发马尔可夫链功率感知系统分析。我们定义了一个功耗感知的时序逻辑和一个模型检查算法[10]，它允许我们检查功耗的界限。我们还可以计算给定时间范围内的最小和最大功耗。2.5多容量资源MCSR扩展了ACSR资源框架，将内存使用作为不同类型的资源来捕获。内存是手机等尺寸受限的嵌入式系统中的关键资源在嵌入式系统的设计中，我们需要考虑系统中内存使用和任务速度之间的多功能资源。内存作为资源的本质与ACSR可串行重用资源不同。两个进程可以使用相同的内存，只要总使用量不超过内存容量。因此，我们引入了一类新的资源，称为多容量资源。具体来说，我们将资源集R划分为类Rs和Rm。R中的资源是由优先级控制的单一能力资源访问，如ACSR。资源类Rm包含多容量资源。Rm中的资源与表示系统中可用资源量的容量属性MCSR中的定时操作。MCSR中的定时动作由根据其类使用的几个资源组成，并且像以前一样，消耗一个时间单位。Rs中的资源与优先级相关联，而Rm中的资源与动作中使用的资源量相关联。例如，对于资源cpu∈Rs，和CPU∈Rm，定时动作{（cpu，i），（CPU，u）}在优先级i使用表示处理器单元的资源cpu，同时消耗表示存储器源的u个单元的资源CPUMCSR系统分析。多容量资源的添加并不影响ACSR的基础模型。因此，为ACSR定义的互模拟因此，我们可以测试通过检查适当的互模拟或搜索死锁状态，对包含多容量资源的实时系统进行优化。226I. Lee等人/理论计算机科学电子笔记162（2006）221引用[1] Ben-Abdallah，H.，“GCSR: A Graphical Language for the Specification, Refinement and Analysis of[2] Bergstra，J. A.，和J. W.克洛普代数与抽象通信过程，理论计算机科学，37：77[3] 布 雷 蒙 德 - 格 雷 戈 伊 雷 普， 和 我 。 Lee ， Proces sAlgebraofC ommunicatinggSh aredRe sorceswithDenseTime and Priorities，Theoretical Computer Science，189：179 -219，1997.[4] 霍尔角A. R.，“Communicating[5] Kwak，H.（英）H、I. Lee，A. Philippou，J. Y. Choi和O. Sokolsky，Symbolic可扩展性分析的实时系统，RTSS'98会议录[6] 我， P. Br'emond-Gr'egoi re和R. Gerber，AProces s-AlgebraicApproachtotheS p epec i ica t i c ati c t i c t i[7] 米尔纳河，[8] Philippou，A.，R. 克里夫兰岛李，S。Smolka和O.陈志华，“实时处理代数中的资源故障”，“计算机科学与工程学报”，2000年第1期，[9] Philippou，A.，O.索科尔斯基和我。李，概率系统的弱互模拟，CONCUR'00会议录[10] Sokolsky ， O. ， A. 菲 利 普 岛 Lee 和 K. Christou ， Modeling and analysis of power-aware systems ，Proceedings of TACAS[11] Vardi，M.，概率并发有限状态程序的自动验证，FOCS'85会议录