时序π演算及其对MARTE顺序图的建模

时序π演算及其对MARTE顺序图的建模 Modeling MARTE Sequence Diagram by a Timing π-Calculus 金暐 JIN Wei 1 first-author 王捍贫 WANG Hanpin 1 曹永知 CAO Yongzhi 1 朱梅霞 ZHU Meixia 1 北京大学信息科学技术学院 北京大学信息科学技术学院 School of Electronics Engineering and Computer Science,Peking University School of Electronics Engineering and Computer Science,Peking University MARTE是统一建模语言UML在实时和嵌入式方面的一个扩展.本文给出π演算的一个带时序的变体来对MARTE顺序图的主要元素进行建模.相对于传统的π演算来说,时序π演算中增加了时间算子,可以对时间的流逝和计时器事件进行描述.同时,给出了时序π演算的语法和语义,并定义了时序π进程间的强互模拟关系.基于时序π演算,定义了MARTE顺序图的形式化模型,从而给出了MARTE顺序图的完整语义,并为进一步的模型检测提供了理论基础. Modeling and Analysis of Real-Time and Embedded Systems（MARTE） are a profile of the Unified Modeling Language（UML） for model driven development of real-time and embedded systems.To describe the MARTE sequence diagrams（MARTE SD） formally,we introduce a new variant of the π-calculus,the timing π-calculus in this paper.With it,we can handle time elapse and timer events.The formalism given in this paper facilitates the reliability analysis and consistency analysis of MARTE SD design processes. 时序π演算 MARTE 顺序图 timing π-calculus MARTE（modeling and analysis of real-time and embedded systems） sequence diagram 10.14188/j.1671-8836.2011.06.008 TP301 国家重点基础研究发展计划（973）项目（82009CB320701,2010CB328103）;国家自然科学基金资助项目（60873061,60821003,61033006） 2011-06-01 2021-04-01 6 57