基于面向方面的实时系统建模方法

分布式实时系统的实时特性可以利用面向方面软件设计方法来建模,把时间方面细分为确定的时间子方面、不确定的时间子方面和模糊时间子方面。根据面向方面技术,不同的时间子方面分别利用随机实时时序逻辑(SQTL)和模糊时间Petri网(FTN)来表示,并且每个不同形式化语言表示的子方面模型能够通过转化为时间自动机织入系统,实现系统的实时特性。

MPSoC核协调可靠性和性能的形式化验证

为了在早期发现片上多核处理器(MPSoC)设计缺陷,提出一种对核协调进行结构建模和性质刻画的形式化方法。在标记变迁系统中引入多项式函数替代动作表达核协调过程中对数据的改变,加入物理元器件发生故障的概率属性,形成用以描述核协调可靠性和性能的混杂马尔科夫决策过程模型。采用随机时序逻辑刻画系统性质,通过模型检测工具验证分析,以银行数据脱敏MPSoC为例,分析系统可靠性和时间延迟与能耗等性能指标。这些验证结果对于早期MPSoC设计人员具有较强的指导作用。

面向方面的时间特性建模

基于面向方面软件设计方法,分离出分布式式系统的时间特性作为一个方面单独建模,将时间子方面思想应用到统一建模语言(UML)建模中,利用随机实时时序逻辑和模糊时间Petri网扩展UML约束。实例证明,该建模方法可解决UML语义问题,使建模更准确,且为日后代码织入、自动生成和测试提供方便。