没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记25(2000)网址:http://www.elsevier.nl/locate/entcs/volume25.html12页通过定时重写形式化和执行消息P. Kosiuczenko,M.Wirsing路德维希-马克西米利安大学信息学院,德国慕尼黑摘要消息序列图(MSC)是一种图形化的跟踪语言,它通过消息交换来描述和规范分布式系统的通信行为(Timed)Maude是一种正式的面向对象的规范语言,它结合了用于描述复杂数据结构的代数规范技术和用于处理动态行为的( Timed ) 项 重 写 在 本 文 中 , 我 们 首 先 展 示 了 如 何 形 式 化 MSC 在TimedMaude。然后,我们给出了定时重写到非定时重写系统的一种翻译,并使用这种翻译在Elan系统上执行消息序列图。Elan系统是一个强大的工具,它结合了重写逻辑和重写策略语言。我们用铁路交叉口的基准示例来说明我们的方法1.导言目前在软件工程中使用的方法采用图形符号,如对象图,场景,消息序列图(MSC)或UML,因为它们的图形表示有助于阅读,理解和系统的设计。然而,这些符号遭受语义问题,因为它们的确切含义往往是不清楚的。最近,通过将形式化技术应用于软件工程实践中使用的方法(例如,[13])。本文是这方面的又一进展我们展示了如何形式化的可执行规范语言Timed Maude的消息序列图,以及如何执行它与Elan系统。1. 这项研究由巴伐利亚研究基金会(Bayerischer Forschungsverbund)资助。出版社:Elsevier Science B. V. 在CC BY-NC-ND许可下开放访问。K OSIUCZENKO 和Wirsing2Maude [2]是一种形式化的面向对象的规范语言,它将用于描述复杂数据结构的代数规范技术与用于处理动态行为的项重写相结合。它基于所谓的重写逻辑(RL)[9],并且具有非常有效的实现。在Maude中,系统组件的通信TimedMaude [7]是Maude的实时扩展,它为Maude的功能视图和过程视图添加了时间视图。它基于定时重写逻辑(TRL),就像Maude基于重写逻辑一样。TRL规格与离散时间可以自动转换为无时间RL规格,我们在本文中显示。MSC [4]是一种图形跟踪语言,用于通过消息交换来描述和指定分布式系统的通信行为。它通过几个结构扩展了交互图,允许组成不同的图。该语言已被国际电信联盟推荐为标准。类似Maude的模型可以用于为MSC提供在本文中,我们展示了如何将基本MSC转换为Timed Maude [5,6]。我们说明我们的方法与基准铁路道口的例子,并提出其正式规范。Elan [1]是一个将重写逻辑与重写策略语言相结合的强大工具。它允许描述和自动执行基于规则的日志系统或过程。它还为用户定义的模块提供了模块化机制我们使用Elan执行MSC图,通过翻译他们的TRL语义Elan的基础上,在RL中的TRL的解释。介绍了如何使用Elan执行、分析和改进铁路道口的MSC规范。我们的方法有几个优点:它提供了MSC的定时重写规范的直接翻译2正式背景。定时重写逻辑(TRL)[7]是重写逻辑(RL)[9]的扩展,用于描述实时系统。它用阿基米德幺半群来模拟时间。时间通过执行重写规则而演变。每个规则由指示执行重写步骤所需的时间TRL的推理规则类似于RL的与RL的主要区别是时间戳的存在,同步替换规则和限制形式(即0-时间)自反性。一个TRL规范是一对形式为(R+),Ax)的规范,其中R+是一个签名,Ax是一组等式和定时重写规则,其形式为:t1-a r->t2,其中a是表示动作或系统步骤的标号,rK OSIUCZENKO 和Wirsing3111是属于基础算术幺半群R2的时间戳,并且t,t是+1 2术语编码系统状态(配置)。TRL有以下演绎规则(加上等式推理规则1. 时间传递性(TT)。 对于每个t1$t2,t3 T(x,X),r1,r2 R+t1---ar1--->t2,t2---br2---> t3t1-a;b r1 +r2-> t32. 同步替换(SR)。 令{x i1,...,xik}= FV(t0)FV(u0)是自由变量t0和u0的交.对于每个t0,...,tn u0 u1,.,unT(x,X), r R+t0-a r-> u0,ti1-ai1 r-> ui,.,tik-aik r-> uikt0(t1,...,tn)-a(ai,.,ai)r-> u0(u1,.,(un)3. 时间相容性=(TCE)。 对于每个t1,t2 <$u1,u2 T(x,X),r1,r2R+,t1=u1,r1 = r2,u1-ar1-> u2,u2= t2t1-a r2-> t24. 0-时间自反性(0-R)。对于每个t T(x,X)t-t 0-> t一个项t被称为静态的,如果它不随时间变化,即。对于所有r,t-t r-> t成立,如果t-a r-> t ′对某个r成立,则t = t ′。如果一个项t不是静态的,那么我们称之为动态的,并将其表示为:op dynamict(参见应用部分)。类似地,排序s是静态的,当且仅当它包含静态项,否则它被称为动态的。TimedMaude是一种基于TRL的面向对象分布式系统的形式化描述它借用了Maude的面向对象概念对象类由标识符和属性及其类型的列表声明对象由一个术语表示,该术语包括唯一的对象名称、对象所属类的标识符以及一组属性及其值。我们将使用大写字母的名称和相应的小写字母的对象是在某些状态表示的常数;例如。 tg = 表示属于TrainGate类的名为TG的对象tg,属性state的值为up。在下面我们经常省略类和属性的名称,而简单地写为.2. 算术幺半群的例子是像自然数这样的离散时间模型以及像实数这样的K OSIUCZENKO 和Wirsing4消息m是一个形式为(X,dt,Y)的项,它由对象名X、Y组成,消息携带的排序数据的名称3和数据DTX和Y可以分别理解为发送方和接收方地址配置是消息和对象的多集(或包)形式上,配置c由以下形式的项表示m1 mk o ol(注:M1)mk o1... ol),其中n是表示多集并的二元函数符号。Timed Maude程序通过重写其状态来进行计算。重写步骤具有以下形式m1... mk o1... ol- a r -> n1. np o1 '. 哦。规则说,在收到消息m1后...出现在规则两侧的对象改变它们的状态,没有出现在右侧的对象被删除,没有出现在左侧的对象被创建,并且消息n1.所有这些都发生在时间r内。3在RL中解释TRL。在本节中,我们将展示如何将(定时的)TRL规范转换为(非定时的)RL规范。原则上,人们也可以选择任何其他术语来重写- malism,但RL由于其与TRL的概念相似而特别方便翻译[11]适用于所有离散时间的线性TRL规范,因此可以应用于比Olveczky和Meseguer [10]的TRL到RL的第一个翻译更一般的TRL规范。3.1 定义.令Sp=(λ(R+),Ax)是任意TRL规范,使得Ax仅包含重写规则,并且每个重写规则具有时间戳0或1。我们定义RL解释Int(Sp)=(Int(Ax(R+)),Int(Ax))如下:对于每个动态排序s,签名Int(R+)用以下新的(多态的)函数符号扩展了R+Go:s-> s,D:s> s,clean:s -> Bool,[_](函数Go(Go代表go)用于标记时间必须进行的动态参数。函数D用于标记时间已经进展的位置(D代表完成)。这些功能允许同步一个术语中函数clean确保一个项被接地并且不包含Go或D。函数[_](-)的第一个参数表示可用于执行规范的时间。2. X、Y也可以是门的名称,参见[8]。K OSIUCZENKO 和Wirsing5重写理论Int(Ax)包含以下规则:规则(i)允许我们在不包含Go或D的项上模拟0次规则;这由clean函数保证。需要清洁条件来确保对0次重写建模的RL规则不应用于通过时间进程的术语部分,因为这可能导致死锁。在某种意义上,规则(ii)允许我们通过一个项向下传播时间。元级项映射用于描述重写项时时间如何进展;它保持静态项不变,而动态项接收新标记:如果时间必须向下传播,则为Go,如果我们准备好子项,则为D。规则(iii)用于使用另一个称为“k”的项映射来提取D函数。(i)对于每一个0次规则t-a 0-> t′ Ax,我们有相应的规则:t -> t ′ ifclean(t),(ii) 对于每一个规则t-a 1-> t′ Ax,我们有相应的条件规则:Go(t)>(t ′),(iii) 对于每个函数符号f:s1,.,sn----------- > s(R+)我们有一个规则要拉出来D功能:f(x1),.,n(xn))-> D(f(x1,,xn))(iv) 最后,对于每个动态排序s和排序s的变量x,我们有一个规则来启动下一个时间步:[n+1](D(x))>[n](Go(x))。clean函数由以下等式公理化:clean(Go(x))=False,clean(D(x))= False,clean(c)= True,clean(f(x1,.,xn))= clean(x1)clean(xn),对于每个常数符号c(R+)和每个n元函数符号f(R+)。术语映射T:T(T(R+),X)----------------------> T(Int(T(R+)),X)定义如下:(1) n(t)= t 如果t是静态排序的成员;(2) n(t)= D(t),如果项t是动态排序的成员,但不包含动态排序的变量;(3) 如果t ≠ x且x是一个动态变量,则Go(t)= Go(x)(其中t ≠ x是语法恒等式);(4) n(t)= f(n(t1),.,tn)) 如果t∈ f(t1,,tn),且t是动态排序的,保持动态排序的变量。映射X:X>T(Int(X(R+)),X)定义为:如果x是静态排序的,则xD(x)= x,否则xD(x)=D(x)。在[11]中,已经证明了在RL中对TRL的解释是正确的,在这个意义上,没有变量的定时重写公式可以从TRL规范推导出来,TRL规范相对于动态变量是线性的,当且仅当它的解释可以从定时规范的非定时解释在RL中推导出来。K OSIUCZENKO 和Wirsing6不TG(8)远起来mcom在0我通过下来远0起来铁路道口MSC4MSC正式成立MSC是一种跟踪语言,用于通过消息交换来描述和规范系统组件及其环境的通信行为[4]。Timed Maude和MSC之间存在有趣的关系,特别是MSC-96存在形式化的Maude类语义[5,6,8]。基本上,MSC图以以下方式描述系统行为[4]:对象(或实例)的行为由定义其动作总顺序的垂直线表示。这样一条垂直线以一个空盒子开始,以一个黑盒子结束。如果一个消息从一个对象发送到另一个对象,则这由从发送者指向接收者的水平箭头指示。消息传递是异步的;因此它对应于两个事件:发送和接收消息。人们可以通过在水平箭头下给出一个实数来MSC的初始(最终)状态是直接发生在MSC的初始(最终)状态之后(或之前)的状态空的(黑色的)盒子MSC实例只能执行三种原子步骤:发送或接收消息,创建或停止另一个对象,以及仅更改对象状态的特殊操作。基本的MSC可以在Timed Maude中形式化如下:对于MSC图的任何实例O,我们引入一个适当类的对象,它包含一个称为状态的属性,即 . 为了简单起见,本文中状态总是不同的对象操作由中间状态分隔。对象状态可以使用由六边形表示的(局部)条件来描述任何发送的消息都被分成发送和接收部分(由“!”和“?”分别)。通常,原子步骤的基础集合L具有形式{?,m,!n,开始,停止,停止,AC1,...,acn},其中“ac最后,我们为任何操作引入重写规则,如下所示:K OSIUCZENKO 和Wirsing7rl< O|状态:s>---!m 0-> m.** 名为O的对象发送消息m,并在0时间内将其状态从s更改为s ′rlm -?m0-> 。** 名为O的对象接收消息m,并在0-time内将其状态从s更改为s ′rlstart(o)---start o 0---> o.** 名为O的对象在0-time内创建rlstop(o)o-stop o 0->停止4.** 对象o在0-time内被删除rl< O|状态:s>-ac i 0-> 。** 名为O的对象执行特殊操作aci,在0-time内更改其状态rlttimer(r1 + r2)-> ttimer(r2)。** 定时器ttimer的值在时间r1减少r1除了最后一种情况之外,我们都说名为O的对象执行了一个动作,例如TG执 行 了动 作 ?mcom) 。 除非另有说明,我们将考虑采取行动的形式t1...tntn)只对ti(x,X),即,仅由一个对象执行的动作或所有组件执行时间步长的规则。为了简单起见,我们将前者写为“a”,后者写为“a”。MSC的时间方面的语义基于以下假设(cf [5]):除非另有说明,否则所有术语都是默认静态的。所有的动作都是一个过程,除了重复,都需要0时间。施加在对象行为或消息传递上的时间约束分别由附加到对象状态或消息的定时器来建模。一个对象可以产生多个并行运行的计时器。原子状态(即状态,没有计时器)可以声明为静态或动态。静态状态可以持续任意长的时间,而动态状态应该立即改变其持续时间为0时间单位)。在本文中,我们假设方程公理只涉及数据携带的消息和多和运算符。形式上,我们定义:4.1定义.MSC规范SP是形式为(R+),Ax,In, Fin)的元组,其中•(R+),Ax)是TRL规范5,使得形成Ax的底层原子标签集合以及重写规则和公理具有上述形式;•In是一组处于初始状态的对象,Fin是一组处于终止状态的对象,这两种状态都是原子的(即由常数表示)。2. 表示空配置。3. 为了简单起见,我们在这里处理(平面)TRL规范,而不是一般的定时MaudeK OSIUCZENKO 和Wirsing8•具有不同名称的对象必须具有不同的状态。配置c= oi1. oik被称为initial(final,resp.),如果In = {0i 1,...,oik}(翅片= {oi1,.,或(分别)。4.2定义.假设SP是MSC规范。一个部分轨迹是一个有限的配置序列,动作,和时间值c0a1 r1 c1.cn-1 an rn cn使得c0是初始配置,ci-ai+1 ri+1-> ci+1,对于i = 0,., n-16。一个部分轨迹是一个轨迹,如果另外cn是最终的配置。一个序列是一个一个二个二...an rn是SP的(部分)迹当且仅当存在形式为c0 a1 r1 c1.的(部分)迹树。cn-1 an rn cn.让我们提到语义允许使用组合操作(如垂直和水平组合)进行组合规范[4]。第一种对应于所谓的弱排序;第二种是一种并行组合,允许指定由并行工作的组件组成的系统[8]。5应用:铁路道口。我们用铁路交叉的基准示例说明我们的方法(例如[3])。首先,我们介绍非正式(文本)规范,然后是它的图形和形式对应物,最后是它的Elan翻译[1]。5.1非正式描述。一个铁路道口由火车门TG和一个带有传感器的火车轨道T组成火车沿着铁轨行驶。当传感器检测到轨道上的进站列车时,它立即将消息mcom发送到列车门。当传感器检测到火车已经通过道口时,它立即将消息m传递到火车门。火车门可以在两个位置:向上,向下。它最初处于向上的位置,在接收到消息m_com后向下移动,在接收到消息m_passed后向上移动。我们对系统行为施加以下时间约束:•一辆远距离的火车需要至少8分钟才能到达大门。2. 让我们指出,在允许门的情况下,定义有点复杂,见[8]。K OSIUCZENKO 和Wirsing9•传感器在列车到达列车门之前检测到列车的到达。一旦它检测到列车到达,它就向列车门发送消息mcom,并且一旦列车通过道口,消息m就通过•火车门立即向下(向上)移动。从位置上(下)在接收到消息m_com(分别为m_passed)之后。•每个消息都立即传递(在0时间内)。5.2正式设计。该系统的抽象设计可以通过消息序列图给出,该图显示了消息流和实时约束。图中给出了显示铁路道口的消息序列图消息传递的时间在对象中设置计时器(例如tfar)由双三角形表示。定时器设置为特定值(tfar设置为值8)。超时由从双三角形开始的箭头指示。Train的行为由对象T(类名为Train)描述我们没有明确地对传感器进行建模,而是将其作为列车规范的一部分列车的属性一列火车最初是在状态远。定时器设置为8个时间单位,确保两列火车之间的8分钟距离。在定时器超时之后的某个时间,发送消息m_com,将T的状态改变为at,指示列车已经到达交叉口。稍后,发送消息mpassed,并且T的状态被设置回far(指示列车已经离开道口)。列车门对象TG(类名称为TGate)的属性存储关于门位置的信息它最初处于向上的位置,在接收到消息mcom后向下移动,然后在接收到消息mcom后向上移动。设消息mcom和mpassed分别为(T,com,g),(T,passed,g)的形式。opfari,far´,at,farf,upi,down,upf:->state,fari,upi:initial,farf,upf:final.**状态是静态的,可以持续任意长时间op dynamiccom,passed:-> data,tfar,:Time-> Timer.** 消息mcom,mpassed将在0时间内传递,因为com,passed被声明为动态的rl< T |far i>-set t far 0-> .** timer t far 8分钟后一列火车可能会来rl< T |t far(0)far i>-t_out t far 0-> .**8分钟过去,计时器超时,列车可能随时出现K OSIUCZENKO 和Wirsing10rl< T |far '>-!m com 0-> m com.**列车检测立即触发发送消息mcom立即rlm com -? m com 0-> 。**收到mcomrl< T |at>-! m通过0-> M通过。**列车通过,立即发送消息m通过rlm通过 -?m通过0->< TG|上f>。** 接收到消息m通过5.3实施.在本小节中,我们将在Elan中实现上述规范该规范由三个模块组成:一个包含基本排序和操作声明的模块模板(由于空间不足,我们跳过了这个模块 ) ,指 定 火 车门 的 模 块tGate_spec ,以及指定整个铁路道口的模块Trains_spec。模块Trains_spec导入模块tGate_spec,后者又导入模板模块。模块tGate_spec涉及列车闸门,它是根据定义3.1的TGate_spec的相应部分的字面翻译模块tGate_spec导入全局模板;结束运算符全局upi : state ; upf : state; down :state ; com:data ; passed:data ;TG:obn ; T:obn ;端全局配置规则[]m(T,com,TG)*< TG| upi> =>< TG|向下>结束[]m(T,通过,TG)*< TG|下> =>< TG |upf>end结束结束对于T的规范,我们遵循解释模式,除了在情况(ii)中,Go的分布性被限制在没有未决消息的配置中,并且计时器中的时间进度被建模为整个对象中的时间进度。第一个变化确保了所有的消息都将在时间推进之前被读取,第二个变化使规范更加紧凑。让我们观察一下,每一个0时间规则只适用于没有变量的项,因此我们不需要清洁函数。K OSIUCZENKO 和Wirsing11模块Trains_specimport global tGate_spec ;end运算符全局fari:state ; far ′:state ; farf:state ; at:state ; t_far(@):(int)timer ;端会议规则s,x,y:state ; c1,c2:conf;n:int ;global[]< T| fari> =>< T| t_far(8)&fari>end[]<不|t_far(0)&fari>=><不|far '>端[]<不|far '>=><不|at > * m(T,com,TG)端[]<不|在>=><不|farf> * m(T,passed,TG)端[]D(c1)* D(c2) =>D(c1 * c2)端[]Go( *< T| y>)=> Go()* Go()end[]Go()=>D()端[]Go()=>D()端[]Go()=>D()if n > 0 end [][n] D(cf)=>[n-1]Go(cf)if n > 0end结束结束Elan实现允许我们执行规范。我们已经从初始配置开始系统地测试了铁路道口规范,输入范围从0到15分钟(铁路道口系统时间)。例如,我们重写了这个术语:[15] D(* )。执行时间为0.380秒。Elan提供了一种追踪重写的可能性通过分析执行跟踪,我们已经观察到,规范,因为它的立场,不禁止消息mcom和m通过之间的竞争,因为第二个消息,sage可以在第一个之前读取。这是因为列车速度没有时间限制。在mcom被读取之前,列车可能在0时间内到达登机口。如果我们确保列车以有限的速度移动,并在指定的时间流逝后到达列车门,则不会发生这种情况;这样的要求K OSIUCZENKO 和Wirsing12可以由另一个计时器指定。Elan实现还提供了更复杂的设施,用于使用内置的策略语言执行规范,可以指定复杂的搜索算法,如深度优先搜索,或约束重写。在今后的工作中K OSIUCZENKO 和Wirsing13我们将使用它来自动检查指定系统的简单时间属性。引用[1]P. Borovansky,C. Kirchner,H. Kirchner,P. -E.莫罗角林盖森ELAN概述。C.Kirchner,H. Kirchner(eds.):1998年WRLA会议记录。《TCS电子注释》,第15卷,Elsevier 1998年。[2]P. M. Clavel,S.Ecker,P.Lincoln,J.梅瑟格尔Maude的原则在j.Meseguer(编辑):李国忠,第一届国际研讨会论文集,第四卷,第65-90页。[3]A.Gabrielian.状态机、时态逻辑和代数数据模型。于T. Rus和C. Rattray(编辑):陈文生,实时系统开发的理论与实践,北京大学出版社,1994。[4]国际电联。ITU-TS,建议Z.120。消息序列图(MSC)。ITU-TS,1996年,日内瓦。[5]P. Kosiuczenko。消息序列图中的时间:一种形式化方法。欧洲Par '97,LNCS1300,1997年,第562-566页。[6]P. Kosiuczenko。MSC-96的形式语义:内联表达式。技术报告编号9705. Ins.fur Informatik,Ludwig-Maximilians-Universität,München,1997,18 pages.[7]P. Kosiuczenko,M.Wirsing。定时重写逻辑及其在基于对象规范中的应用计算机程序设计科学28(2-3),1997,第225-246页。[8]P. Kosiuczenko,M. Wirsing。信息序列图与定时Maude的集成。1998年7月6日至9日在柏林举行的IDPT会议记录。[9]J. 梅瑟格尔作为并发统一模型的条件重写逻辑理论计算机科学96,1992,第158-200页。[10] P. Olveczky,J. Meseguer.实时系统重写逻辑。In J. Mesequer(ed.):重写逻辑及其应用。TCS中的电子注释,4。第一次国际研讨会,太平洋格罗夫,C。一、1996年9月[11] J. Steggles,P.科修琴科基于时间重写逻辑的SDL规范形式化模型自动化软件工程,Kluver,2000年。[12] M. Wirsing。代数规范。在J.范Leeuwen(编辑):《理论计算机科学手册》,阿姆斯特丹,北荷兰,1990年,第675-788页。[13] M. Wirsing,A.纳普面向对象软件工程的形式化方法。在j.Meseguer(编辑):重写逻辑及其应用。第一届国际研讨会,TCS中的电子注释,第4卷,1996年,第321-359页。
下载后可阅读完整内容,剩余1页未读,立即下载
![rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![application/msword](https://img-home.csdnimg.cn/images/20210720083327.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- VMP技术解析:Handle块优化与壳模板初始化
- C++ Primer 第四版更新:现代编程风格与标准库
- 计算机系统基础实验:缓冲区溢出攻击(Lab3)
- 中国结算网上业务平台:证券登记操作详解与常见问题
- FPGA驱动的五子棋博弈系统:加速与创新娱乐体验
- 多旋翼飞行器定点位置控制器设计实验
- 基于流量预测与潮汐效应的动态载频优化策略
- SQL练习:查询分析与高级操作
- 海底数据中心散热优化:从MATLAB到动态模拟
- 移动应用作业:MyDiaryBook - Google Material Design 日记APP
- Linux提权技术详解:从内核漏洞到Sudo配置错误
- 93分钟快速入门 LaTeX:从入门到实践
- 5G测试新挑战与罗德与施瓦茨解决方案
- EAS系统性能优化与故障诊断指南
- Java并发编程:JUC核心概念解析与应用
- 数据结构实验报告:基于不同存储结构的线性表和树实现
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)