VERTAF: an application framework for the design and verification of embedded real-time software

The growing complexity of embedded real-time software requirements calls for the design of reusable software components, the synthesis and generation of software code, and the automatic guarantee of nonfunctional properties such as performance, time constraints, reliability, and security. Available application frameworks targeted at the automatic design of embedded real-time software are poor in integrating functional and nonfunctional requirements. To bridge this gap, we reveal the design flow and the internal architecture of a newly proposed framework called verifiable embedded real-time application framework (VERTAF), which integrates software component-based reuse, formal synthesis, and formal verification. A formal UML-based embedded real-time object model is proposed for component reuse. Formal synthesis employs quasistatic and quasidynamic scheduling with automatic generation of multilayer portable efficient code. Formal verification integrates a model checker kernel from SGM, by adapting it for embedded software. The proposed architecture for VERTAF is component-based and allows plug-and-play for the scheduler and the verifier. Using VERTAF to develop application examples significantly reduced design effort and illustrated how high-level reuse of software components combined with automatic synthesis and verification can increase design productivity.     

Automatic synthesis and verification of real-time embedded software for mobile and ubiquitous systems

Currently available application frameworks that target the automatic design of real-time embedded software are poor in integrating functional and non-functional requirements for mobile and ubiquitous systems. In this work, we present the internal architecture and design flow of a newly proposed framework called Verifiable Embedded Real-Time Application Framework (VERTAF), which integrates three techniques namely software component-based reuse, formal synthesis, and formal verification. Component reuse is based on a formal unified modeling language (UML) real-time embedded object model. Formal synthesis employs quasi-static and quasi-dynamic scheduling with multi-layer portable efficient code generation, which can output either real-time operating systems (RTOS)-specific application code or automatically generated real-time executive with application code. Formal verification integrates a model checker kernel from state graph manipulators (SGM), by adapting it for embedded software. The proposed architecture for VERTAF is component-based which allows plug-and-play for the scheduler and the verifier. The architecture is also easily extensible because reusable hardware and software design components can be added. Application examples developed using VERTAF demonstrate significantly reduced relative design effort as compared to design without VERTAF, which also shows how high-level reuse of software components combined with automatic synthesis and verification increases design productivity.     

一种基于嵌入式软件构件管理方法

构件化软件开发的最终目的是希望软件像传统产品一样能在生产线上生产出来。软件最终由软件框架来实现,一个良好的软件框架应该能够将设计结果尽量保存下来,同时可以灵活更换和重用软件部件。研究构件化的软件框架对构件化的开发技术在嵌入式实时软件开发中迅速普及具有最直接的推动作用。对嵌入式控制系统嵌入软件构件框架进行了深入研究,完成了框架中的数据管理和构件调度机制等内容,验证了该源码构件模型在嵌入式控制软件领域中的可用性。     

实时嵌入式环境中面向构件系统的QoS模型研究

将基于构件技术的开发引入到实时嵌入式软件平台能够很好地适应嵌入式领域多样性的特点,满足对软件开发效率和软件质量的要求。为保证实时嵌入式环境对资源动态变化的需求，考虑到系统资源的全局管理特性，仅从应用中增加QoS适应机制是不够的，还需在现有的构件框架中增加QoS管理机制。为此，提出了一种面向CCM构件系统的QoS模型，能够主动适应动态变化的资源状态，模型中层次式的QoS转换器的设计简化了用户对服务的QoS参数配置。     

在构件化嵌入式操作系统中应用抢占阈值调度

现有基于构件的嵌入式实时软件开发过程着重于从结构的角度分解系统成若干构件,以及重用构件。实践证明,该开发过程还应从运行角度将构件映射成任务,并选择适当的实时调度算法。为此,根据目前的工程实践提出一种实时构件模型,包含将构件映射成任务的方式。描述了当前构件化嵌入式操作系统可以使用的4种调度算法,并比较这些算法的性能特点。提出抢占阈值(preemptionthreshold)调度模型更适合构件化嵌入式实时系统,仿真实验的结果证明了该结论。比较结果和结论对构件化嵌入式实时系统的设计和开发有一定的参考价值。     

构件化动态政府门户通用平台的研究与应用

基于构件的软件开发可以复用已有的应用系统、应用框架,开发出具有良好的可维护性和软件资源的可复用性,并有较强的用户需求变化适应能力的软件。构件的可复用性越高、复用越广泛,其复用次数就会越多,价值也越大。该文研究了基于构件的通用政府门户平台,提出了基于构件的政务通门户系统开发框架,可重用构件是其重要的一部分。该门户平台类似于一个网站生成器,通过简单的拖拉拽等操作就可以完成不同政府的门户平台系统的生成工作。     

Verifying distributed real-time properties of embedded systems via graph transformations and model checking

Component middleware provides dependable and efficient platforms that support key functional, and quality of service (QoS) needs of distributed real-time embedded (DRE) systems. Component middleware, however, also introduces challenges for DRE system developers, such as evaluating the predictability of DRE system behavior, and choosing the right design alternatives before committing to a specific platform or platform configuration. Model-based technologies help address these issues by enabling design-time analysis, and providing the means to automate the development, deployment, configuration, and integration of component-based DRE systems. To this end, this paper applies model checking techniques to DRE design models using model transformations to verify key QoS properties of component-based DRE systems developed using Real-time CORBA. We introduce a formal semantic domain for a general class of DRE systems that enables the verification of distributed non-preemptive real-time scheduling. Our results show that model-based techniques enable design-time analysis of timed properties and can be applied to effectively predict, simulate, and verify the event-driven behavior of component-based DRE systems. This research was supported by the NSF Grants CCR-0225610 and ACI-0204028 Gabor Madl is a Ph.D. student and a graduate student researcher at the Center for Embedded Computer Systems at the University of California, Irvine. His advisor is Nikil Dutt. His research interests include the formal verification, optimization, component-based composition, and QoS management of distributed real-time embedded systems. He received his M.S. in computer science from Vanderbilt University and in computer engineering from the Budapest University of Technology and Economics. Dr. Sherif Abdelwahed received his Ph.D. degree in Electrical and Computer Engineering from the University of Toronto, Canada, in 2001. During 2000–2001, he was a research scientist with the system diagnosis group at the Rockwell Scientific Company. Since 2001 he has been with the Department of Electrical Engineering and Computer Science at Vanderbilt University as a Research Assistant Professor. His research interests include verification and control of distributed real-time systems, and model-based diagnosis of discrete-event and hybrid systems. Dr. Douglas C. Schmidt is a Professor of Computer Science, Associate Chair of the Computer Science and Engineering program, and a Senior Researcher in the Institute for Software Integrated Systems (ISIS) all at Vanderbilt University. He has published over 300 technical papers and 6 books that cover a range of research topics, including patterns, optimization techniques, and empirical analyses of software frameworks and domain-specific modeling environments that facilitate the development of distributed real-time and embedded (DRE) middleware and applications. Dr. Schmidt has served as a Deputy Office Director and a Program Manager at DARPA, where he lead the national R&D effort on middleware for DRE systems. In addition to his academic research and government service, Dr. Schmidt has over fifteen years of experience leading the development of ACE, TAO, CIAO, and CoSMIC, which are widely used, open-source DRE middleware frameworks and model-driven tools that contain a rich set of components and domain-specific languages that implement patterns and product-line architectures for high-performance DRE systems.     

面向方面的实时系统形式化开发方法

实时系统复杂性的不断增加以及对可配置性和可重用性要求的不断提高,需要如面向方面和基于组件的软件工程方法的支持,同时实时系统的可信性要求采用形式化方法来开发实时系统。本文试图建立一种面向方面的实时系统形式化开发方法,这种方法对RT—Z进行了面向方面和面向部件的扩展,并通过实时组件模型在需求和设计阶段提供了对基于部件的系统开发方法(CBSD)和面向方面的系统开发方法(AOSD)的支持。本文给出了面向方面的实时Z(AO—RT—Z)的组件模型的框架结构、语法要求、方面的联结和功能接口和非功能接口的定义,重点讨论并证明了面向方面的实时Z(AO—RT—Z)作为规格描述语言的健全性。     

A design flow for supporting component-based software development in multiprocessor real-time systems

Component-based software development established as an effective technique to cope with the increasing complexity of modern computing systems. In the context of real-time systems, the M-BROE framework has been recently proposed to efficiently support component-based development of real-time applications on multiprocessor platforms in the presence of shared resources. The framework relies on a two-stage approach where software components are first partitioned upon a virtual multiprocessor platform and are later integrated upon the physical platform by means of component interfaces that abstract from the internal details of the applications. This work presents a complete design flow for the M-BROE framework. Starting from a model of software components, a first method is proposed to partition applications to virtual processors and perform a synthesis of multiple component interfaces. Then, a second method is proposed to support the integration of the components by allocating virtual processors to physical processors. Both methods take resource sharing into account. Experimental results are also presented to evaluate the proposed methodology.     

面向网络处理器的软件组件框架研究

网络处理器通常由多个异构的处理和内存单元通过片上网络连接构成,其目标应用需要在Gbit/s到几十Gbit/s的网络环境中以线速处理数据包。基于网络处理器的应用有实时、资源受限和异构的特点。组件技术对于复杂的嵌入式系统是一种十分有前途的方法。本文以一种典型的网络处理器为例,说明了在基于网络处理器的系统中应用组件技术时,对组件框架的要求,讨论了组件组合框架和运行时框架,并定义了组件框架服务。利用提出的组件框架,可以实现软件性能工程。     

嵌入式应用中运行支撑框架的构件化技术研究

为增强嵌入式软件的复用性、可移植性,缩短开发周期,通过研究现有的主流构件运行支撑技术,提出了一种面向嵌入式领域的运行支撑体系结构。为实现灵活、开放的嵌入式应用平台,本文首先建立了构件化的嵌入式运行支撑框架模型,然后结合PDA手机领域重点分析了开放式HLA结构和虚拟OS平台等关键技术,最后利用伪代码示例探讨了该领域中应用平台的定制与扩展方法。     

Communications-oriented development of component-based vehicular distributed real-time embedded systems

We propose a novel model- and component-based technique to support communications-oriented development of software for vehicular distributed real-time embedded systems. The proposed technique supports modeling of legacy nodes and communication protocols by encapsulating and abstracting the internal implementation details and protocols. It also allows modeling and performing timing analysis of the applications that contain network traffic originating from outside of the system such as vehicle-to-vehicle, vehicle-to-infrastructure, and cloud-based applications. Furthermore, we present a method to extract end-to-end timing models to support end-to-end timing analysis. We also discuss and solve the issues involved during the extraction of these models. As a proof of concept, we implement our technique in the Rubus Component Model which is used for the development of software for vehicular embedded systems by several international companies. We also conduct an application-case study to validate our approach.     

基于任务间通信的嵌入式组件模型

通用组件技术如COM、CORBA等技术已较完善,但是它们应用于嵌入式系统却有很多局限,如需要庞大的底层基础支持、没有实时调度能力等。根据嵌入式系统以及应用的特点,分析了现有的通用组件模型和当前嵌入式组件技术的发展现状,提出了一种新的嵌入式组件模型——基于任务间通信的嵌入式组件模型。该模型具有资源消耗小、有实时调度能力、无须大量底层支持的优点,该文介绍了系统框架和实现方法以及组件开发方法。     

面向构件化软件的合约检查测试框架

基于构件软件开发的主要思想是使用现存的构件来建构软件系统。而这样的系统由于构件本身的特点导致了许多测试困难。B. Meyer将构件与其客户代码之间的关系形式化地定义为一种合约,它严格限定了构件对象之间的交互规则。通过对合约的监视和检查,可以容易地发现构件之间的交互错误,从而达到集成测试构件化软件的目的。该文提出了一种基于合约检查的构件集成测试框架 (contract-checking test framework,CCTF)。讨论了该框架合约检查的思想、5大功能模块以及其测试流程,并介绍了将CCTF应用到构件化软件测试平台实现的一些关键技术。     

Performance and energy consumption estimation for commercial off-the-shelf component system design

Nowadays, component-based embedded real- time systems have been used to improve the system development as well as to keep cost down through the reuse of embedded software applications. Besides, the use of semi-formal models has been widely adopted in the embedded real-time system component and system life cycle due to their friendly and intuitive notations. However, the ever more complex systems of today require modeling methods that allow early detection of potential problems in the initial phases of development. This paper presents the mapping process of UML state machine diagram into a time Petri net with energy constraints so as to estimate execution time and energy consumption in early phases of the embedded real-time component development life cycle. The estimates obtained from the model show that the proposed approach is indeed a good approximation to the respective measures obtained from the real hardware platform.     

基于C/S关系的实时系统构件交互规约

给出了基于构件的实时多任务应用系统图形化设计软件的构件接口定义。为解决基于构件的分布式C/S关系的实时软件构件的重用及装配问题,提出了构件相互交互的文本描述语言语法语义规约,其主要刻画了分布式实时构件之间的交互协议及其实时特性。     

基于构件的信息系统开发框架

本文在研究了基于构件的信息系统体系结构基础上，提出了基于构件的信息系统的开发框架，其中可重用构件是其重要的一部分。该框架可以看作是一个基于构件的“标准”的原型系统，类似于一个构件化信息系统产生器，通过该框架可迅速生成一个构件化的信息系统。     

构件软件测试技术研究进展

软构件技术提供了一种较面向对象方法更为有效的软件设计模式,构件软件被广泛应用并成为一种主流软件形态．然而,构件的内部信息屏蔽、演变速度快以及构件间的异质、松耦合等特点给构件软件系统的测试带来极大的挑战,寻求高效的构件软件测试技术和开发实用的测试工具是当今软件业界一个亟待解决的课题．分析和归纳近年来一些典型的构件、构件软件测试方法和技术并对当前较为有效的测试框架和工具进行总结;最后,对其今后若干研究方向进行了展望．     

Models and temporal logical specifications for timed component connectors

Component-based software engineering advocates construction of software systems through composition of coordinated autonomous components. Significant benefits of this approach include software reuse, simpler and faster construction, enhanced reliability, and dramatic reductions in the complexity of construction of provably correct critical systems, many of which involve real-time concerns. Effective, flexible component composition by itself still poses a challenge today and yet the special nature of real-time constraints makes component-based construction of real-time systems even more demanding. The coordination language Reo supports compositional system construction through connectors that exogenously coordinate the interactions among the constituent components which unawarely comprise a complex system, into a coherent collaboration. The simple, yet surprisingly rich, calculus of channel composition that underlies Reo offers a flexible framework for compositional construction of coordinating component connectors with real-time properties. In this paper, we present an operational semantics for the channel-based component connectors of Reo in terms of Timed Constraint Automata and introduce a temporal-logic for specification and verification of their real-time properties.      

实时系统构件非功能性接口语义规约

该文给出了基于构件的实时多任务应用系统图形化设计软件的具有分布式C/S关系实时构件的接口定义,主要论述实时构件非功能性接口模型,针对实时特性,提出构件的非功能性接口在时间性、调度性、合成性、同步、互斥以及资源设备控制方面的语义规约。