基于UML的嵌入式系统建模及模型验证机制研究

统一建模语言UML在嵌入式系统设计建模中已经获得了广泛的认可，并有很多成功的应用，但UML存在时间约束描述能力不强和所建模型形式化复杂、验证难的问题。针对上述问题，本文提出了使用UML扩展机制对UML状态图进行时间扩展，建立系统状态一约束一事件矩阵来对模型进行形式化描述的方法。该方法解决了UML在嵌入式系统建模时存在的问题。应用实例和实验结果验证了该方法的可行性和有效性。     

一种嵌入式系统设计的建模方法研究

针对在嵌入式系统设计中,目前常用的VHDL建模方法方法存在不易理解、模型描述困难、工作量大的问题,UML建模方法存在模型需形式化、验证难等问题,提出了一种基于SpecCharts语言的嵌入式系统建模方法--使用SpecCharts语言语法、文字和图形相结合来描述嵌入式系统,能满足嵌入式系统设计的描述要求,建模效率是VHDL方法的2.82倍,是UML方法的1.25倍,并且具有容易理解、容易描述、能利用VHDL的支撑工具直接进行模拟验证、建模工作量小等优点,较好地解决了嵌入式系统设计建模中存在的上述问题,有较高的实用价值.     

嵌入式建模中带有时间扩展的UML状态图的形式化方法

面向对象建模语言UML(Unified Modeling Language)已广泛用于嵌入式系统建模,但它在嵌入式实时系统建模时存在概念模型形式化复杂和状态图对时间约束方面的建模功能不强的问题,针对这些问题,提出一种对UML状态图进行时间扩展的方法,并提出利用"可执行UML"对带有时间扩展的UML状态图形式化的方法.     

基于UML-OCPN的嵌入式系统建模

针对统一建模语言（UML）缺乏精确的形式化的语义描述而不能对其所建模型进行分析和验证的难题,提出一种改进的建模方法——UML-OCPN方法。该方法结合UML和对象着色Petri网（OCPN）的优点,使用UML进行建模,将其转换为Petri网模型再进行模型验证。实验结果证明,该方法能较好地解决单一使用UML或Petri网建模时出现的无法进行验证、需要开发人员具备较高数学水平等问题。     

使用时间化自动机形式化带有时间扩展的UML状态图

严格建模是嵌入式实时系统设计的核心技术，通过UMI。方法与形式化方法结合可以给严格建模提供很好的工具支持。时间化自动机(Timed Automata)是一种用于描述、验证实时系统的理论模型。文中提出了一种通过时间化自动机来形式化带有时间扩展的UML状态图的方法，这种方法为UMI。与形式化方法的结合构造了桥梁作用。带有时间扩展的UML状态图用于嵌入式系统动态模型的建模，从时间化自动机模型得到形式化规范将更容易。UML状态图的形式化分为两部分完成；层次状态图的平面化以及时间化自动机的构造。     

基于UML的嵌入式系统模型验证机制的研究

随着嵌入式系统在各个领域的广泛应用,嵌入式系统变得越来越复杂,研究一种支持嵌入式系统从分析、设计、验证到编码这一整个开发过程的模型系统及建模方法变得越来越重要。UML(UnifiedModelingLanguage,统一建模语言)作为面向对象的分析与设计技术的代表,已经获得了广泛的承认,并在多个领域中有成功的应用。然而,UML是一种符号化语言系统,其语义采用自然语言描述,没有完全形式化,无法精确和严格地描述模型的行为从而实现模型的验证。为了解决这个问题,文章提出了一种用于嵌入式系统UML模型验证的方法,其核心是可执行(Executable)UML,它是UML的增强性子集,采用与UML相同的符号表示法,并集成了状态图(StateChart)所用的形式化语义定义。嵌入式系统的UML模型经过语义分析能够很方便地生成可执行UML模型,并实现系统模型的验证。     

基于扩展Petri网的系统建模及形式化验证方法*

嵌入式实时系统对时间约束性、安全性和可靠性具有非常高的要求,但是传统的建模和形式化验证方法难以满足对系统的实时性和安全性的模拟和验证需求。通过对有色Petri网的时间属性进行扩展,提出了实时有色Petri网模型,能够对系统的时间属性进行模拟和评估;参考实时有色Petri网模型到时间自动机的语义转换规则对模型进行转换,可以利用时间计算树逻辑对系统的实时性、安全性和可靠性进行形式化验证。以列车通信网络控制器的双线冗余控制模块的建模和形式化验证为例,证明了该方法的有效性。     

使用UML对μC/OS-Ⅱ建模与分析

使用统一建模语言(UML)对嵌入式实时操作系统μC/OS-Ⅱ做静态建模和动态建模,进而利用UML的可视化模型来描述和分析μC/OS-Ⅱ的系统结构和工作机理.通过UML静态建模,为基于μC/OS-Ⅱ的嵌入式系统设计,提供了一个运用面向对象技术的框架;通过UML动态建模,详细分析了嵌入式实时操作系统(ERTOS)的关键方面,包括实时内核的调度机理、优先级反转问题及其解决办法等.     

基于等级PRES+的嵌入式系统的建模与实现

为了有效的描绘规模较大的系统,需要一个分层机制,使模型可以有条理地构建.它由简单的单元组件构成,使得设计师在每个描述级上都可以很容易理解.提出并定义了用于形式化描述嵌入式系统建模的petri网的分层概念,显示了一个规模较大系统中的小部件如何使用层次的概念进行转换.该方法使得复杂的嵌入式系统描述更加模块化,具有可重用性,提高了嵌入式系统建模和分析的效率.通过一个实例表明了该方法的可行性.     

使用UML对μC/OS-II建模与分析

使用统一建模语言（UML）对嵌入式实时操作系统C/OS-II做静态建模和动态建模,进而利用UML的可视化模型来描述和分析C/OS-II的系统结构和工作机理。通过UML静态建模,为基于C/OS-II的嵌入式系统设计,提供了一个运用面向对象技术的框架;通过UML动态建模,详细分析了嵌入式实时操作系统（ERTOS）的关键方面,包括实时内核的调度机理、优先级反转问题及其解决办法等。     

嵌入式实时控制系统软件可靠性建模与应用

嵌入式实时控制系统(ERCS)广泛应用于各种控制系统中,其软件不同于普通软件,除满足实时性要求外,可靠性也是相当重要的。首先对嵌入式实时控制系统软件进行形式化抽象定义,然后对不可再分的软件模块进行可靠性建模,并应用Copula函数对软件系统进行建模,最后应用建立的模型,对具体的系统进行了软件可靠性计算。通过实例计算可知,用Copula函数建立的嵌入式实时控制系统软件可靠性模型,考虑了软件各个模块的相依性,进而得到嵌入式实时控制系统软件模块相依的可靠度较各模块独立时有所提高。     

Hybrid MARTE statecharts

The specification of modeling and analysis of real-time and embedded systems (MARTE) is an extension of the unified modeling language (UML) in the domain of real-time and embedded systems. Even though MARTE time model offers a support to describe both discrete and dense clocks, the biggest effort has been put so far on the specification and analysis of discrete MARTE models. To address hybrid real-time and embedded systems, we propose to extend statecharts using both MARTE and the theory of hybrid automata. We call this extension hybrid MARTE statecharts. It provides an improvement over the hybrid automata in that: the logical time variables and the chronometric time variables are unified. The formal syntax and semantics of hybrid MARTE statecharts are given based on labeled transition systems and live transition systems. As a case study, we model the behavior of a train control system with hybrid MARTE statecharts to demonstrate the benefit.     

An approach for machine-assisted verification of Timed CSP specifications

The real-time process calculus Timed CSP is capable of expressing properties such as deadlock-freedom and real-time constraints. It is therefore well-suited to model and verify embedded software. However, proofs about Timed CSP specifications are not ensured to be correct since comprehensive machine-assistance for Timed CSP is not yet available. In this paper, we present our formalization of Timed CSP in the Isabelle/HOL theorem prover, which we have formulated as an operational coalgebraic semantics together with bisimulation equivalences and coalgebraic invariants. This allows for semi-automated and mechanically checked proofs about Timed CSP specifications. Mechanically checked proofs enhance confidence in verification because corner cases cannot be overlooked. We additionally apply our formalization to an abstract specification with real-time constraints. This is the basis for our current work, in which we verify a simple real-time operating system deployed on a satellite. As this operating system has to cope with arbitrarily many threads, we use verification techniques from the area of parameterized systems for which we outline their formalization.     

Clock constraint specification language: specifying clock constraints with UML/MARTE

The Object Management Group (OMG) unified modeling language (UML) profile for modeling and analysis of real-time and embedded systems (MARTE) aims at using the general-purpose modeling language UML in the domain of real-time and embedded (RTE) systems. To achieve this goal, it is absolutely required to introduce inside the mainly untimed UML an unambiguous time structure which MARTE model elements can rely on to build precise models amenable to formal analysis. The MARTE Time model has defined such a structure. We have also defined a non-normative concrete syntax called the clock constraint specification language (CCSL) to demonstrate what can be done based on this structure. This paper gives a brief overview of this syntax and its formal semantics, and shows how existing UML model elements can be used to apply this syntax in a graphical way and benefit from the semantics.     

反射式集成框架的规约描述方法研究

反射式集成框架的规约描述方法,主要研究在分布式实时应用领域基于构件的软件开发模式中集成框架的形式化规约描述问题.这种描述方法通过引入反射技术,除了描述集成框架中组成要素的业务逻辑之外,还对各要素的实时性能约束、运行时状态的变化以及可能具有的需求变更等特征进行形式化规约,从而支持软件在需求分析阶段的演化进程,并以指导与实现实时应用软件开发时业务逻辑与系统非功能性特征的关注分离.     

Dealing with different time granularities in formal specifications of real-time systems

The article presents a formalization of the notion of time granularity within a logical language for specifying real-time systems. It provides the specifier with the ability of dealing with different time granularities within a single specification. That is, it allows the specifier to describe the behavior and the properties of a system and its environment with respect to different time scales and to switch among them in a suitable way. The extended logical formalism is then embedded in an object oriented structure that enhances both the expressive power and the executability of the specification language. With regard to expressiveness, it enables one to subdivide a single specification of the system and its environment into different part and to provide a number of specifications of them at different levels of abstraction, each one referring to a different time granularity. With regard to executability, it allows one to verify the consistency and the adequacy of specifications at each step of their incremental development. It also suggests an enlargement of the notions of verification and validation that takes into account the stratified structure of the object oriented specifications.     

基于UML和CPN的列控系统等级转换建模与分析

针对列控系统的安全性和实时性要求,基于CTCS-3级列控系统需求规范中等级转换场景建立C2级向C3级转换的UML(统一建模语言)模型和有色Petri网(CPN)模型,分析了影响列车安全运行和行车效率的因素,即转换时长和转换成功率,验证了该建模方法的有效性。验证结果表明,UML和CPN模型相结合的方法适合于列控系统需求规范的验证。搭建的等级转换模型能够满足系统实时性要求。在保证切换成功率的前提下,列车运行速度与切换时间成反比,速度越高,切换时间越短;列车速度越高,对系统实时性要求也越高。